Lemmas for the field_simp tactic

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.

theorem Mathlib.Tactic.FieldSimp.zpow'_add {α : Type u_1} [GroupWithZero α] (a : α) (m n : ℤ) : zpow' a (m + n) = zpow' a m * zpow' a n

theorem Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_right {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) (hn : n ≠ 0) : zpow' a n = a ^ n

theorem Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_left {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) (ha : a ≠ 0) : zpow' a n = a ^ n

@[simp]

theorem Mathlib.Tactic.FieldSimp.zero_zpow' {α : Type u_1} [GroupWithZero α] (n : ℤ) : zpow' 0 n = 0

theorem Mathlib.Tactic.FieldSimp.zpow'_eq_zero_iff {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) : zpow' a n = 0 ↔ a = 0

@[simp]

theorem Mathlib.Tactic.FieldSimp.one_zpow' {α : Type u_1} [GroupWithZero α] (n : ℤ) : zpow' 1 n = 1

@[simp]

theorem Mathlib.Tactic.FieldSimp.zpow'_one {α : Type u_1} [GroupWithZero α] (a : α) : zpow' a 1 = a

theorem Mathlib.Tactic.FieldSimp.zpow'_zero_eq_div {α : Type u_1} [GroupWithZero α] (a : α) : zpow' a 0 = a / a

theorem Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero {α : Type u_1} [GroupWithZero α] {a : α} (ha : a ≠ 0) : zpow' a 0 = 1

theorem Mathlib.Tactic.FieldSimp.zpow'_neg {α : Type u_1} [GroupWithZero α] (a : α) (n : ℤ) : zpow' a (-n) = (zpow' a n)⁻¹

theorem Mathlib.Tactic.FieldSimp.zpow'_mul {α : Type u_1} [GroupWithZero α] (a : α) (m n : ℤ) : zpow' a (m * n) = zpow' (zpow' a m) n

theorem Mathlib.Tactic.FieldSimp.zpow'_ofNat {α : Type u_1} [GroupWithZero α] (a : α) {n : ℕ} (hn : n ≠ 0) : zpow' a ↑n = a ^ n

theorem Mathlib.Tactic.FieldSimp.mul_zpow' {α : Type u_1} [CommGroupWithZero α] (n : ℤ) (a b : α) : zpow' (a * b) n = zpow' a n * zpow' b n

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

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

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

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

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⁻¹

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

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

theorem Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq {M : Type u_1} [MonoidWithZero M] [IsLeftCancelMulZero M] {e₁ e₂ f₁ f₂ L : M} (H₁ : e₁ = L * f₁) (H₂ : e₂ = L * f₂) (HL : L ≠ 0) : (e₁ = e₂) = (f₁ = f₂)

theorem Mathlib.Tactic.FieldSimp.le_eq_cancel_le {M : Type u_1} [MonoidWithZero 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₂)

theorem Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt {M : Type u_1} [MonoidWithZero 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.

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.

@[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.

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.

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.

@[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

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

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

theorem Mathlib.Tactic.FieldSimp.NF.atom_eq_eval {M : Type u_1} [GroupWithZero M] (x : M) : x = eval [(1, x)]

theorem Mathlib.Tactic.FieldSimp.NF.one_eq_eval (M : Type u_1) [GroupWithZero M] : 1 = eval []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance Mathlib.Tactic.FieldSimp.NF.instInv {M : Type u_1} : Inv (NF M)

theorem Mathlib.Tactic.FieldSimp.NF.eval_inv {M : Type u_1} [CommGroupWithZero M] (l : NF M) : l⁻¹.eval = l.eval⁻¹

theorem Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval {M : Type u_1} [CommGroupWithZero M] (l : NF M) : 1 / l.eval = l⁻¹.eval

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

instance Mathlib.Tactic.FieldSimp.NF.instPowInt {M : Type u_1} : Pow (NF M) ℤ

@[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

theorem Mathlib.Tactic.FieldSimp.NF.eval_zpow' {M : Type u_1} [CommGroupWithZero M] (l : NF M) (r : ℤ) : (l ^ r).eval = zpow' l.eval r

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

instance Mathlib.Tactic.FieldSimp.NF.instPowNat {M : Type u_1} : Pow (NF M) ℕ

@[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

theorem Mathlib.Tactic.FieldSimp.NF.eval_pow {M : Type u_1} [CommGroupWithZero M] (l : NF M) (r : ℕ) : (l ^ r).eval = zpow' l.eval ↑r

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

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

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

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

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.

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.

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.

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⁻¹.

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.

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.

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.

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.

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.

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.