# Lemmas for the field_simp tactic #

source
noncomputable def Mathlib.Tactic.FieldSimp.zpow' {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) :
α

This is a variant of integer exponentiation, defined for internal use in the `field_simp` tactic implementation. It differs from the usual integer exponentiation in that `0 ^ 0` is `0`, not `1`. With this choice, the function `n ↦ a ^ n` is always a homomorphism (`a ^ (n + m) = a ^ n * a ^ m`), even if `a` is zero.

Equations

- Mathlib.Tactic.FieldSimp.zpow' a n = if a = 0 ∧ n = 0 then 0 else a ^ n

Instances For

source
theorem Mathlib.Tactic.FieldSimp.zpow'_add {α : Type u_1} [GroupWithZero α] (a : α) (m n : ℤ) :
zpow' a (m + n) = zpow' a m * zpow' a n
source
theorem Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_right {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) (hn : n ≠ 0) :
zpow' a n = a ^ n
source
theorem Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_left {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) (ha : a ≠ 0) :
zpow' a n = a ^ n
source
@[simp]
theorem Mathlib.Tactic.FieldSimp.zero_zpow' {α : Type u_1} [GroupWithZero α] (n : ℤ) :
zpow' 0 n = 0
source
theorem Mathlib.Tactic.FieldSimp.zpow'_eq_zero_iff {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) :
zpow' a n = 0 ↔ a = 0
source
@[simp]
theorem Mathlib.Tactic.FieldSimp.one_zpow' {α : Type u_1} [GroupWithZero α] (n : ℤ) :
zpow' 1 n = 1
source
@[simp]
theorem Mathlib.Tactic.FieldSimp.zpow'_one {α : Type u_1} [GroupWithZero α] (a : α) :
zpow' a 1 = a
source
theorem Mathlib.Tactic.FieldSimp.zpow'_zero_eq_div {α : Type u_1} [GroupWithZero α] (a : α) :
zpow' a 0 = a / a
source
theorem Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero {α : Type u_1} [GroupWithZero α] {a : α} (ha : a ≠ 0) :
zpow' a 0 = 1
source
theorem Mathlib.Tactic.FieldSimp.zpow'_neg {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) :
zpow' a (-n) = (zpow' a n)⁻¹
source
theorem Mathlib.Tactic.FieldSimp.zpow'_mul {α : Type u_1} [GroupWithZero α] (a : α) (m n : ℤ) :
zpow' a (m * n) = zpow' (zpow' a m) n
source
theorem Mathlib.Tactic.FieldSimp.zpow'_ofNat {α : Type u_1} [GroupWithZero α] (a : α) {n : ℕ} (hn : n ≠ 0) :
zpow' a ↑n = a ^ n
source
theorem Mathlib.Tactic.FieldSimp.mul_zpow' {α : Type u_1} [CommGroupWithZero α] (n : ℤ) (a b : α) :
zpow' (a * b) n = zpow' a n * zpow' b n
source
theorem Mathlib.Tactic.FieldSimp.list_prod_zpow' {α : Type u_1} [CommGroupWithZero α] {r : ℤ} {l : List α} :
zpow' l.prod r = (List.map (fun (x : α) => zpow' x r) l).prod
source
theorem Mathlib.Tactic.FieldSimp.subst_add {M : Type u_1} [Semiring M] {x₁ x₂ X₁ X₂ Y y a : M} (h₁ : x₁ = a * X₁) (h₂ : x₂ = a * X₂) (H_atom : X₁ + X₂ = Y) (hy : a * Y = y) :
x₁ + x₂ = y
source
theorem Mathlib.Tactic.FieldSimp.subst_sub {M : Type u_1} [Ring M] {x₁ x₂ X₁ X₂ Y y a : M} (h₁ : x₁ = a * X₁) (h₂ : x₂ = a * X₂) (H_atom : X₁ - X₂ = Y) (hy : a * Y = y) :
x₁ - x₂ = y
source
theorem Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst {M : Type u_1} [DivInvOneMonoid M] {l l_n n : M} (h : l = l_n / 1) (hn : l_n = n) :
l = n
source
theorem Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst' {M : Type u_1} [DivInvOneMonoid M] {l l_d d : M} (h : l = 1 / l_d) (hn : l_d = d) :
l = d⁻¹
source
theorem Mathlib.Tactic.FieldSimp.eq_div_of_subst {M : Type u_1} [Div M] {l l_n l_d n d : M} (h : l = l_n / l_d) (hn : l_n = n) (hd : l_d = d) :
l = n / d
source
theorem Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul {M : Type u_1} [Mul M] {a b c D e f : M} (h₁ : a = b) (h₂ : b = c) (h₃ : c = D * e) (h₄ : e = f) :
a = D * f
source
theorem Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq {M : Type u_1} [CancelMonoidWithZero M] {e₁ e₂ f₁ f₂ L : M} (H₁ : e₁ = L * f₁) (H₂ : e₂ = L * f₂) (HL : L ≠ 0) :
(e₁ = e₂) = (f₁ = f₂)
source
theorem Mathlib.Tactic.FieldSimp.le_eq_cancel_le {M : Type u_1} [CancelMonoidWithZero M] [PartialOrder M] [PosMulMono M] [PosMulReflectLE M] {e₁ e₂ f₁ f₂ L : M} (H₁ : e₁ = L * f₁) (H₂ : e₂ = L * f₂) (HL : 0 < L) :
(e₁ ≤ e₂) = (f₁ ≤ f₂)
source
theorem Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt {M : Type u_1} [CancelMonoidWithZero M] [PartialOrder M] [PosMulStrictMono M] [PosMulReflectLT M] {e₁ e₂ f₁ f₂ L : M} (H₁ : e₁ = L * f₁) (H₂ : e₂ = L * f₂) (HL : 0 < L) :
(e₁ < e₂) = (f₁ < f₂)

### Theory of lists of pairs (exponent, atom) #

This section contains the lemmas which are orchestrated by the `field_simp` tactic to prove goals in fields. The basic object which these lemmas concern is `NF M`, a type synonym for a list of ordered pairs in `ℤ × M`, where typically `M` is a field.

source
def Mathlib.Tactic.FieldSimp.NF (M : Type u_1) :
Type u_1

Basic theoretical "normal form" object of the `field_simp` tactic: a type synonym for a list of ordered pairs in `ℤ × M`, where typically `M` is a field. This is the form to which the tactics reduce field expressions.

Equations

- Mathlib.Tactic.FieldSimp.NF M = List (ℤ × M)

Instances For

source
@[match_pattern]
def Mathlib.Tactic.FieldSimp.NF.cons {M : Type u_1} (p : ℤ × M) (l : NF M) :
NF M

Augment a `FieldSimp.NF M` object `l`, i.e. a list of pairs in `ℤ × M`, by prepending another pair `p : ℤ × M`.

Equations

- p ::ᵣ l = p :: l

Instances For

source
def Mathlib.Tactic.FieldSimp.NF.«term_::ᵣ_» :
Lean.TrailingParserDescr

Augment a `FieldSimp.NF M` object `l`, i.e. a list of pairs in `ℤ × M`, by prepending another pair `p : ℤ × M`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
noncomputable def Mathlib.Tactic.FieldSimp.NF.eval {M : Type u_1} [GroupWithZero M] (l : NF M) :
M

Evaluate a `FieldSimp.NF M` object `l`, i.e. a list of pairs in `ℤ × M`, to an element of `M`, by forming the "multiplicative linear combination" it specifies: raise each `M` term to the power of the corresponding `ℤ` term, then multiply them all together.

Equations

- l.eval = (List.map (fun (x : ℤ × M) => match x with | (r, x) => Mathlib.Tactic.FieldSimp.zpow' x r) l).prod

Instances For

source
@[simp]
theorem Mathlib.Tactic.FieldSimp.NF.eval_cons {M : Type u_1} [CommGroupWithZero M] (p : ℤ × M) (l : NF M) :
(p ::ᵣ l).eval = l.eval * zpow' p.2 p.1
source
theorem Mathlib.Tactic.FieldSimp.NF.cons_ne_zero {M : Type u_1} [GroupWithZero M] (r : ℤ) {x : M} (hx : x ≠ 0) {l : NF M} (hl : l.eval ≠ 0) :
((r, x) ::ᵣ l).eval ≠ 0
source
theorem Mathlib.Tactic.FieldSimp.NF.cons_pos {M : Type u_1} [GroupWithZero M] [PartialOrder M] [PosMulStrictMono M] [PosMulReflectLT M] [ZeroLEOneClass M] (r : ℤ) {x : M} (hx : 0 < x) {l : NF M} (hl : 0 < l.eval) :
0 < ((r, x) ::ᵣ l).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.atom_eq_eval {M : Type u_1} [GroupWithZero M] (x : M) :
x = eval [(1, x)]
source
theorem Mathlib.Tactic.FieldSimp.NF.one_eq_eval (M : Type u_1) [GroupWithZero M] :
1 = eval []
source
theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ {M : Type u_1} [CommGroupWithZero M] (a₁ : ℤ × M) {a₂ : ℤ × M} {l₁ l₂ l : NF M} (h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval) :
(a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ {M : Type u_1} [CommGroupWithZero M] (r₁ r₂ : ℤ) (x : M) {l₁ l₂ l : NF M} (h : l₁.eval * l₂.eval = l.eval) :
((r₁, x) ::ᵣ l₁).eval * ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ {M : Type u_1} [CommGroupWithZero M] {a₁ : ℤ × M} (a₂ : ℤ × M) {l₁ l₂ l : NF M} (h : (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval) :
(a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval {M : Type u_1} [GroupWithZero M] {l₁ l₂ l : NF M} {x₁ x₂ : M} (hx₁ : x₁ = l₁.eval) (hx₂ : x₂ = l₂.eval) (h : l₁.eval * l₂.eval = l.eval) :
x₁ * x₂ = l.eval
source
theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ {M : Type u_1} [CommGroupWithZero M] (a₁ : ℤ × M) {a₂ : ℤ × M} {l₁ l₂ l : NF M} (h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval) :
(a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ {M : Type u_1} [CommGroupWithZero M] (r₁ r₂ : ℤ) (x : M) {l₁ l₂ l : NF M} (h : l₁.eval / l₂.eval = l.eval) :
((r₁, x) ::ᵣ l₁).eval / ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ {M : Type u_1} [CommGroupWithZero M] {a₁ : ℤ × M} (a₂ : ℤ × M) {l₁ l₂ l : NF M} (h : (a₁ ::ᵣ l₁).eval / l₂.eval = l.eval) :
(a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval {M : Type u_1} [GroupWithZero M] {l₁ l₂ l : NF M} {x₁ x₂ : M} (hx₁ : x₁ = l₁.eval) (hx₂ : x₂ = l₂.eval) (h : l₁.eval / l₂.eval = l.eval) :
x₁ / x₂ = l.eval
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons {M : Type u_1} [CommGroupWithZero M] (n : ℤ) (e : M) {L l l' : NF M} (h : L.eval * l.eval = l'.eval) :
L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero {M : Type u_1} [CommGroupWithZero M] {e : M} {L l l' l₀ : NF M} (h : L.eval * l.eval = l'.eval) (h' : ((0, e) ::ᵣ l).eval = l₀.eval) :
L.eval * l₀.eval = ((0, e) ::ᵣ l').eval
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval {M : Type u_1} [CommGroupWithZero M] (n : ℤ) (e : M) {L l l' : NF M} (h : L.eval * l.eval = l'.eval) :
((n, e) ::ᵣ L).eval * l.eval = ((n, e) ::ᵣ l').eval
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg {M : Type u_1} [CommGroupWithZero M] (n : ℤ) {e : M} (he : e ≠ 0) {L l l' : NF M} (h : L.eval * l.eval = l'.eval) :
((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval
source
theorem Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div {M : Type u_1} [CommGroupWithZero M] (n : ℤ) (e : M) {t t_n t_d : NF M} (h : t.eval = t_n.eval / t_d.eval) :
((n, e) ::ᵣ t).eval = ((n, e) ::ᵣ t_n).eval / t_d.eval
source
theorem Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' {M : Type u_1} [CommGroupWithZero M] (n : ℤ) (e : M) {t t_n t_d : NF M} (h : t.eval = t_n.eval / t_d.eval) :
((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.cons_zero_eq_div_of_eq_div {M : Type u_1} [CommGroupWithZero M] (e : M) {t t_n t_d : NF M} (h : t.eval = t_n.eval / t_d.eval) :
((0, e) ::ᵣ t).eval = ((1, e) ::ᵣ t_n).eval / ((1, e) ::ᵣ t_d).eval
source
instance Mathlib.Tactic.FieldSimp.NF.instInv {M : Type u_1} :
Inv (NF M)
Equations

- One or more equations did not get rendered due to their size.

source
theorem Mathlib.Tactic.FieldSimp.NF.eval_inv {M : Type u_1} [CommGroupWithZero M] (l : NF M) :
l⁻¹.eval = l.eval⁻¹
source
theorem Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval {M : Type u_1} [CommGroupWithZero M] (l : NF M) :
1 / l.eval = l⁻¹.eval
source
theorem Mathlib.Tactic.FieldSimp.NF.inv_eq_eval {M : Type u_1} [CommGroupWithZero M] {l : NF M} {x : M} (h : x = l.eval) :
x⁻¹ = l⁻¹.eval
source
instance Mathlib.Tactic.FieldSimp.NF.instPowInt {M : Type u_1} :
Pow (NF M) ℤ
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Mathlib.Tactic.FieldSimp.NF.zpow_apply {M : Type u_1} (r : ℤ) (l : NF M) :
l ^ r = List.map (fun (x : ℤ × M) => match x with | (a, x) => (r * a, x)) l
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_zpow' {M : Type u_1} [CommGroupWithZero M] (l : NF M) (r : ℤ) :
(l ^ r).eval = zpow' l.eval r
source
theorem Mathlib.Tactic.FieldSimp.NF.zpow_eq_eval {M : Type u_1} [CommGroupWithZero M] {l : NF M} {r : ℤ} (hr : r ≠ 0) {x : M} (hx : x = l.eval) :
x ^ r = (l ^ r).eval
source
instance Mathlib.Tactic.FieldSimp.NF.instPowNat {M : Type u_1} :
Pow (NF M) ℕ
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Mathlib.Tactic.FieldSimp.NF.pow_apply {M : Type u_1} (r : ℕ) (l : NF M) :
l ^ r = List.map (fun (x : ℤ × M) => match x with | (a, x) => (↑r * a, x)) l
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_pow {M : Type u_1} [CommGroupWithZero M] (l : NF M) (r : ℕ) :
(l ^ r).eval = zpow' l.eval ↑r
source
theorem Mathlib.Tactic.FieldSimp.NF.pow_eq_eval {M : Type u_1} [CommGroupWithZero M] {l : NF M} {r : ℕ} (hr : r ≠ 0) {x : M} (hx : x = l.eval) :
x ^ r = (l ^ r).eval
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero {M : Type u_1} [CommGroupWithZero M] {r : ℤ} (hr : r = 0) {x : M} (hx : x ≠ 0) (l : NF M) :
((r, x) ::ᵣ l).eval = l.eval
source
theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq {M : Type u_1} [CommGroupWithZero M] (r : ℤ) (x : M) {t t' l' : NF M} (h : t.eval = t'.eval) (h' : ((r, x) ::ᵣ t').eval = l'.eval) :
((r, x) ::ᵣ t).eval = l'.eval

### Negations of algebraic operations #

source
inductive Mathlib.Tactic.FieldSimp.Sign {v : Lean.Level} (M : Q(Type v)) :
Type

Inductive type representing the options for the sign of an element in a type-expression `M`

If the sign is "-", then we also carry an expression for a field instance on `M`, to allow us to construct that negation when needed.

- plus {v : Lean.Level} {M : Q(Type v)} : Sign M
- minus {v : Lean.Level} {M : Q(Type v)} (iM : Q(Field «$M»)) : Sign M

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.expr {v : Lean.Level} {M : Q(Type v)} :
Sign M → Q(«$M») → Q(«$M»)

Given an expression `e : Q($M)`, construct an expression which is morally "± `e`", with the choice between + and - determined by an object `g : Sign M`.

Equations

- Mathlib.Tactic.FieldSimp.Sign.plus.expr x✝ = x✝
- (Mathlib.Tactic.FieldSimp.Sign.minus iM).expr x✝ = q(-$x✝)

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.mulRight {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (c y : Q(«$M»)) (g : Sign M) :
Lean.MetaM (have a := g.expr y; have a_1 := g.expr q(«$c» * «$y»); Q(«$a_1» = «$c» * «$a»))

Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that the product with `c` of (± `y`) (here taking the specified sign) is ± `c * y`.

Equations

- Mathlib.Tactic.FieldSimp.Sign.mulRight iM c y Mathlib.Tactic.FieldSimp.Sign.plus = pure q(⋯)
- Mathlib.Tactic.FieldSimp.Sign.mulRight iM c y (Mathlib.Tactic.FieldSimp.Sign.minus iM_1) = pure q(⋯)

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.mul {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y₁ y₂ : Q(«$M»)) (g₁ g₂ : Sign M) :
Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y₁» * «$y₂»); have a_1 := g₂.expr y₂; have a_2 := g₁.expr y₁; Q(«$a_2» * «$a_1» = «$a»))

Given expressions `y₁ y₂ : Q($M)` with specified signs (either + or -), construct a proof that the product of (± `y₁`) and (± `y₂`) (here taking the specified signs) is ± `y₁ * y₂`; return this proof and the computed sign.

Equations

- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus (Mathlib.Tactic.FieldSimp.Sign.minus i) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus i) Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.mul iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus iM_1) (Mathlib.Tactic.FieldSimp.Sign.minus iM_2) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.inv {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y : Q(«$M»)) (g : Sign M) :
Lean.MetaM (have a := g.expr q(«$y»⁻¹); have a_1 := g.expr y; Q(«$a_1»⁻¹ = «$a»))

Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that the inverse of (± `y`) (here taking the specified sign) is ± `y⁻¹`.

Equations

- Mathlib.Tactic.FieldSimp.Sign.inv iM y Mathlib.Tactic.FieldSimp.Sign.plus = pure q(⋯)
- Mathlib.Tactic.FieldSimp.Sign.inv iM y (Mathlib.Tactic.FieldSimp.Sign.minus iM_1) = pure q(⋯)

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.div {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y₁ y₂ : Q(«$M»)) (g₁ g₂ : Sign M) :
Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y₁» / «$y₂»); have a_1 := g₂.expr y₂; have a_2 := g₁.expr y₁; Q(«$a_2» / «$a_1» = «$a»))

Given expressions `y₁ y₂ : Q($M)` with specified signs (either + or -), construct a proof that the quotient of (± `y₁`) and (± `y₂`) (here taking the specified signs) is ± `y₁ / y₂`; return this proof and the computed sign.

Equations

- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ Mathlib.Tactic.FieldSimp.Sign.plus (Mathlib.Tactic.FieldSimp.Sign.minus i) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus i) Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus i, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.div iM y₁ y₂ (Mathlib.Tactic.FieldSimp.Sign.minus iM_1) (Mathlib.Tactic.FieldSimp.Sign.minus iM_2) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.neg {v : Lean.Level} {M : Q(Type v)} (iM : Q(Field «$M»)) (y : Q(«$M»)) (g : Sign M) :
Lean.MetaM ((G : Sign M) × have a := G.expr y; have a_1 := g.expr y; Q(-«$a_1» = «$a»))

Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that the negation of (± `y`) (here taking the specified sign) is ∓ `y`.

Equations

- Mathlib.Tactic.FieldSimp.Sign.neg iM y Mathlib.Tactic.FieldSimp.Sign.plus = pure ⟨Mathlib.Tactic.FieldSimp.Sign.minus iM, q(⋯)⟩
- Mathlib.Tactic.FieldSimp.Sign.neg iM y (Mathlib.Tactic.FieldSimp.Sign.minus iM_1) = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.pow {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y : Q(«$M»)) (g : Sign M) (s : ℕ) :
Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y» ^ «$s»); have a_1 := g.expr y; Q(«$a_1» ^ «$s» = «$a»))

Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that the exponentiation to power `s : ℕ` of (± `y`) (here taking the specified signs) is ± `y ^ s`; return this proof and the computed sign.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.FieldSimp.Sign.pow iM y Mathlib.Tactic.FieldSimp.Sign.plus s = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.zpow {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y : Q(«$M»)) (g : Sign M) (s : ℤ) :
Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y» ^ «$s»); have a_1 := g.expr y; Q(«$a_1» ^ «$s» = «$a»))

Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that the exponentiation to power `s : ℤ` of (± `y`) (here taking the specified signs) is ± `y ^ s`; return this proof and the computed sign.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.FieldSimp.Sign.zpow iM y Mathlib.Tactic.FieldSimp.Sign.plus s = pure ⟨Mathlib.Tactic.FieldSimp.Sign.plus, q(⋯)⟩

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.congr {v : Lean.Level} {M : Q(Type v)} {y y' : Q(«$M»)} (g : Sign M) (pf : Q(«$y» = «$y'»)) :
have a := g.expr y'; have a_1 := g.expr y; Q(«$a_1» = «$a»)

Given a proof that two expressions `y₁ y₂ : Q($M)` are equal, construct a proof that (± `y₁`) and (± `y₂`) are equal, where the same sign is taken in both expression.

Equations

- Mathlib.Tactic.FieldSimp.Sign.plus.congr pf = pf
- (Mathlib.Tactic.FieldSimp.Sign.minus iM).congr pf = q(⋯)

Instances For

source
def Mathlib.Tactic.FieldSimp.Sign.mkEqMul {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) {a b C d e : Q(«$M»)} {g : Sign M} (pf₁ : have a_1 := g.expr b; Q(«$a» = «$a_1»)) (pf₂ : Q(«$b» = «$C» * «$d»)) (pf₃ : Q(«$d» = «$e»)) :
Lean.MetaM (have a_1 := g.expr e; Q(«$a» = «$C» * «$a_1»))

If `a` = ± `b`, `b = C * d`, and `d = e`, construct a proof that `a` = `C` * ± `e`.

Equations

- One or more equations did not get rendered due to their size.

Instances For