awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
pos : ∀ (ha : a = 0), zpow' (a * b) n = zpow' a n * zpow' b n
neg : ∀ (ha : ¬a = 0), zpow' (a * b) n = zpow' a n * zpow' b n
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
ha : a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
simp [ha]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
pos : ∀ (hb : b = 0), zpow' (a * b) n = zpow' a n * zpow' b n
neg : ∀ (hb : ¬b = 0), zpow' (a * b) n = zpow' a n * zpow' b n
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
simp [hb]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
simpa [zpow', ha, hb] using mul_zpow a b n

Premises used: mul_zpow, Mathlib.Tactic.FieldSimp.zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
α : Type u_1
inst : CommGroupWithZero α
r : ℤ
l : List α
⊢ zpow' l.prod r = prod (map (fun (x : α) ↦ zpow' x r) l)

Tactic:
let fr : α →* α := ⟨⟨fun b ↦ zpow' b r, one_zpow' r⟩, (mul_zpow' r)⟩
  map_list_prod fr l

Premises used: Mathlib.Tactic.FieldSimp.one_zpow', OneHom.mk, MonoidHom.mk, map_list_prod, Mathlib.Tactic.FieldSimp.zpow', Mathlib.Tactic.FieldSimp.mul_zpow', ite
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : 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
subst : a * X₁ + a * X₂ = a * (X₁ + X₂)
⊢ x₁ + x₂ = y

Tactic:
subst h₁ h₂ H_atom hy
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : Semiring M
X₁ X₂ a : M
⊢ a * X₁ + a * X₂ = a * (X₁ + X₂)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : 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
subst : a * X₁ - a * X₂ = a * (X₁ - X₂)
⊢ x₁ - x₂ = y

Tactic:
subst h₁ h₂ H_atom hy
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : Ring M
X₁ X₂ a : M
⊢ a * X₁ - a * X₂ = a * (X₁ - X₂)

Tactic:
simp [mul_sub]

Premises used: mul_sub
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
rw : l_n / 1 = n
rw₁ : n / 1 = n
rw₂ rw₃ : n = n
⊢ l = n

Tactic:
rw [h, hn, div_one]

Premises used: div_one
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : DivInvOneMonoid M
l l_d d : M
h : l = 1 / l_d
hn : l_d = d
rw : 1 / l_d = d⁻¹
rw₁ : 1 / d = d⁻¹
rw₂ rw₃ : d⁻¹ = d⁻¹
⊢ l = d⁻¹

Tactic:
rw [h, hn, one_div]

Premises used: one_div
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
rw : l_n / l_d = n / d
rw₁ : n / l_d = n / d
rw₂ rw₃ : n / d = n / d
⊢ l = n / d

Tactic:
rw [h, hn, hd]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
rw : b = D * f
rw₁ : c = D * f
rw₂ : D * e = D * f
rw₃ rw₄ : D * f = D * f
⊢ a = D * f

Tactic:
rw [h₁, h₂, h₃, h₄]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : L ≠ 0
subst : (L * f₁ = L * f₂) = (f₁ = f₂)
⊢ (e₁ = e₂) = (f₁ = f₂)

Tactic:
subst H₁ H₂
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
f₁ f₂ L : M
HL : L ≠ 0
rw rw₁ : (f₁ = f₂) = (f₁ = f₂)
⊢ (L * f₁ = L * f₂) = (f₁ = f₂)

Tactic:
rw [mul_right_inj' HL]

Premises used: mul_right_inj'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulMono M
inst_3 : PosMulReflectLE M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
subst : (L * f₁ ≤ L * f₂) = (f₁ ≤ f₂)
⊢ (e₁ ≤ e₂) = (f₁ ≤ f₂)

Tactic:
subst H₁ H₂
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulMono M
inst_3 : PosMulReflectLE M
f₁ f₂ L : M
HL : 0 < L
a : L * f₁ ≤ L * f₂ ↔ f₁ ≤ f₂
⊢ (L * f₁ ≤ L * f₂) = (f₁ ≤ f₂)

Tactic:
apply Iff.eq

Premises used: Iff.eq
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulMono M
inst_3 : PosMulReflectLE M
f₁ f₂ L : M
HL : 0 < L
⊢ L * f₁ ≤ L * f₂ ↔ f₁ ≤ f₂

Tactic:
mul_le_mul_iff_right₀ HL

Premises used: mul_le_mul_iff_right₀
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulMono M
inst_3 : PosMulReflectLE M
f₁ f₂ L : M
HL : 0 < L
⊢ L * f₁ ≤ L * f₂ ↔ f₁ ≤ f₂

Tactic:
exact mul_le_mul_iff_right₀ HL

Premises used: mul_le_mul_iff_right₀
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
subst : (L * f₁ < L * f₂) = (f₁ < f₂)
⊢ (e₁ < e₂) = (f₁ < f₂)

Tactic:
subst H₁ H₂
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
f₁ f₂ L : M
HL : 0 < L
a : L * f₁ < L * f₂ ↔ f₁ < f₂
⊢ (L * f₁ < L * f₂) = (f₁ < f₂)

Tactic:
apply Iff.eq

Premises used: Iff.eq
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
f₁ f₂ L : M
HL : 0 < L
⊢ L * f₁ < L * f₂ ↔ f₁ < f₂

Tactic:
mul_lt_mul_iff_of_pos_left HL

Premises used: mul_lt_mul_iff_of_pos_left
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
f₁ f₂ L : M
HL : 0 < L
⊢ L * f₁ < L * f₂ ↔ f₁ < f₂

Tactic:
exact mul_lt_mul_iff_of_pos_left HL

Premises used: mul_lt_mul_iff_of_pos_left
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
p : ℤ × M
l : NF M
unfold :
  prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        (p :: l)) =
    prod
        (map
          (fun (x : ℤ × M) ↦
            match (motive := ℤ × M → M) x with
            | (r, x) => zpow' x r)
          l) *
      zpow' p.2 p.1
⊢ (p ::ᵣ l).eval = l.eval * zpow' p.2 p.1

Tactic:
unfold eval cons

Premises used: Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
p : ℤ × M
l : NF M
⊢ prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        (p :: l)) =
    prod
        (map
          (fun (x : ℤ × M) ↦
            match (motive := ℤ × M → M) x with
            | (r, x) => zpow' x r)
          l) *
      zpow' p.2 p.1

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
apply :
  Ne.{u_1 + 1} (α := M)
    ((fun (x : ℤ × M) ↦
        (match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r :
          M))
      (r, x))
    0
⊢ Ne (α := M)
    (prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)))
    0

Tactic:
apply mul_ne_zero ?_ hl

Premises used: mul_ne_zero
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ Ne.{u_1 + 1} (α := M)
    ((fun (x : ℤ × M) ↦
        (match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r :
          M))
      (r, x))
    0

Tactic:
simp [zpow'_eq_zero_iff, hx]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_eq_zero_iff
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
inst_4 : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
unfold :
  LT.lt (α := M) 0
    (prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)))
⊢ 0 < ((r, x) ::ᵣ l).eval

Tactic:
unfold eval cons

Premises used: Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
inst_4 : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
apply :
  LT.lt.{u_1} (α := M) 0
    ((fun (x : ℤ × M) ↦
        (match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r :
          M))
      (r, x))
⊢ LT.lt (α := M) 0
    (prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)))

Tactic:
apply mul_pos ?_ hl

Premises used: mul_pos
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
inst_4 : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
simp : 0 < zpow' x r
⊢ LT.lt.{u_1} (α := M) 0
    ((fun (x : ℤ × M) ↦
        (match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r :
          M))
      (r, x))

Tactic:
simp only
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
inst_4 : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
rw : 0 < x ^ r
⊢ 0 < zpow' x r

Tactic:
rw [zpow'_of_ne_zero_left _ _ hx.ne']

Premises used: LT.lt.ne', Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_left
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : PartialOrder M
inst_2 : PosMulStrictMono M
inst_3 : PosMulReflectLT M
inst_4 : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < x ^ r

Tactic:
apply zpow_pos hx

Premises used: zpow_pos
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
x : M
⊢ x = eval [(1, x)]

Tactic:
simp [eval]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : GroupWithZero M
⊢ Eq.{u_1 + 1} (α := M) 1 (eval [])

Tactic:
(rfl)

Premises used: Mathlib.Tactic.FieldSimp.NF.eval, List.foldr, rfl, List.prod
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval
simp : l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1) = l₁.eval * (l₂.eval * zpow' a₂.2 a₂.1) * zpow' a₁.2 a₁.1
⊢ (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval
⊢ l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1) = l₁.eval * (l₂.eval * zpow' a₂.2 a₂.1) * zpow' a₁.2 a₁.1

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval * l₂.eval = l.eval
simp : l₁.eval * zpow' x r₁ * (l₂.eval * zpow' x r₂) = l₁.eval * l₂.eval * (zpow' x r₁ * zpow' x r₂)
⊢ ((r₁, x) ::ᵣ l₁).eval * ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h, zpow'_add]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_add, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval * l₂.eval = l.eval
⊢ l₁.eval * zpow' x r₁ * (l₂.eval * zpow' x r₂) = l₁.eval * l₂.eval * (zpow' x r₁ * zpow' x r₂)

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval
simp : l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1) = l₁.eval * zpow' a₁.2 a₁.1 * l₂.eval * zpow' a₂.2 a₂.1
⊢ (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval
⊢ l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1) = l₁.eval * zpow' a₁.2 a₁.1 * l₂.eval * zpow' a₂.2 a₂.1

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : 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
rw : l₁.eval * x₂ = l.eval
rw₁ : l₁.eval * l₂.eval = l.eval
rw₂ rw₃ : l.eval = l.eval
⊢ x₁ * x₂ = l.eval

Tactic:
rw [hx₁, hx₂, h]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval
simp :
  l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1)⁻¹ = l₁.eval * (l₂.eval * zpow' a₂.2 a₂.1)⁻¹ * zpow' a₁.2 a₁.1
⊢ (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval
⊢ l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1)⁻¹ = l₁.eval * (l₂.eval * zpow' a₂.2 a₂.1)⁻¹ * zpow' a₁.2 a₁.1

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval / l₂.eval = l.eval
simp : l₁.eval * zpow' x r₁ * (l₂.eval⁻¹ * zpow' x (-r₂)) = l₁.eval * l₂.eval⁻¹ * (zpow' x r₁ * zpow' x (-r₂))
⊢ ((r₁, x) ::ᵣ l₁).eval / ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

Tactic:
simp only [← h, eval_cons, div_eq_mul_inv, mul_inv, ← zpow'_neg, sub_eq_add_neg, zpow'_add]

Premises used: mul_inv, sub_eq_add_neg, div_eq_mul_inv, Mathlib.Tactic.FieldSimp.zpow'_neg, Mathlib.Tactic.FieldSimp.zpow'_add, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval / l₂.eval = l.eval
⊢ l₁.eval * zpow' x r₁ * (l₂.eval⁻¹ * zpow' x (-r₂)) = l₁.eval * l₂.eval⁻¹ * (zpow' x r₁ * zpow' x (-r₂))

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ 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

Tactic:
simp only [eval_cons, ← h, zpow'_neg, div_eq_mul_inv, mul_inv, mul_assoc]

Premises used: mul_inv, mul_assoc, div_eq_mul_inv, Mathlib.Tactic.FieldSimp.zpow'_neg, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : 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
rw : l₁.eval / x₂ = l.eval
rw₁ : l₁.eval / l₂.eval = l.eval
rw₂ rw₃ : l.eval = l.eval
⊢ x₁ / x₂ = l.eval

Tactic:
rw [hx₁, hx₂, h]
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
rw : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = ((n, e) ::ᵣ l').eval
rw₁ : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = l'.eval * zpow' (n, e).2 (n, e).1
rw₂ : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = L.eval * l.eval * zpow' (n, e).2 (n, e).1
rw₃ rw₄ : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = L.eval * (l.eval * zpow' (n, e).2 (n, e).1)
⊢ L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval

Tactic:
rw [eval_cons, eval_cons, ← h, mul_assoc]

Premises used: mul_assoc, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
e : M
L l l' l₀ : NF M
h : L.eval * l.eval = l'.eval
h' : ((0, e) ::ᵣ l).eval = l₀.eval
rw : L.eval * l₀.eval = L.eval * ((0, e) ::ᵣ l).eval
rw₁ rw₂ : L.eval * l₀.eval = L.eval * l₀.eval
⊢ L.eval * l₀.eval = ((0, e) ::ᵣ l').eval

Tactic:
rw [← eval_mul_eval_cons 0 e h, h']

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons, OfNat.ofNat
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
rw : L.eval * zpow' (n, e).2 (n, e).1 * l.eval = L.eval * l.eval * zpow' (n, e).2 (n, e).1
⊢ ((n, e) ::ᵣ L).eval * l.eval = ((n, e) ::ᵣ l').eval

Tactic:
rw [eval_cons, eval_cons, ← h]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ L.eval * zpow' (n, e).2 (n, e).1 * l.eval = L.eval * l.eval * zpow' (n, e).2 (n, e).1

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
rw : ((n + -n, e) ::ᵣ l').eval = l'.eval
⊢ ((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval

Tactic:
rw [mul_eq_eval₂ n (-n) e h]

Premises used: Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂, Neg.neg
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n + -n, e) ::ᵣ l').eval = l'.eval

Tactic:
simp [zpow'_zero_of_ne_zero he]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
simp : t_n.eval * t_d.eval⁻¹ * zpow' e n = t_n.eval * zpow' e n * t_d.eval⁻¹
⊢ ((n, e) ::ᵣ t).eval = ((n, e) ::ᵣ t_n).eval / t_d.eval

Tactic:
simp only [eval_cons, h, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ t_n.eval * t_d.eval⁻¹ * zpow' e n = t_n.eval * zpow' e n * t_d.eval⁻¹

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
simp : t_n.eval * t_d.eval⁻¹ * (zpow' e n)⁻¹ = t_n.eval * (t_d.eval⁻¹ * (zpow' e n)⁻¹)
⊢ ((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval

Tactic:
simp only [eval_cons, h, zpow'_neg, div_eq_mul_inv, mul_inv]

Premises used: mul_inv, div_eq_mul_inv, Mathlib.Tactic.FieldSimp.zpow'_neg, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ t_n.eval * t_d.eval⁻¹ * (zpow' e n)⁻¹ = t_n.eval * (t_d.eval⁻¹ * (zpow' e n)⁻¹)

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
simp : t_n.eval * t_d.eval⁻¹ * (zpow' e 1 * zpow' e (-1)) = t_n.eval * zpow' e 1 * (t_d.eval⁻¹ * zpow' e (-1))
⊢ ((0, e) ::ᵣ t).eval = ((1, e) ::ᵣ t_n).eval / ((1, e) ::ᵣ t_d).eval

Tactic:
simp only [eval_cons, h, div_eq_mul_inv, mul_inv, ← zpow'_neg, ← add_neg_cancel (1:ℤ), zpow'_add]

Premises used: add_neg_cancel, mul_inv, div_eq_mul_inv, Mathlib.Tactic.FieldSimp.zpow'_neg, Mathlib.Tactic.FieldSimp.zpow'_add, OfNat.ofNat, Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ t_n.eval * t_d.eval⁻¹ * (zpow' e 1 * zpow' e (-1)) = t_n.eval * zpow' e 1 * (t_d.eval⁻¹ * zpow' e (-1))

Tactic:
ac_rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
simp :
  Eq (α := M) (prod (map ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (-x.1, x.2)) l))
    (prod (map ((fun (x : M) ↦ x⁻¹) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) l))
⊢ l⁻¹.eval = l.eval⁻¹

Tactic:
simp +instances only [NF.eval, List.map_map, NF.instInv, List.prod_inv]

Premises used: List.map_map, Mathlib.Tactic.FieldSimp.NF.instInv, Mathlib.Tactic.FieldSimp.NF.eval, List.prod_inv
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
h :
  Eq.{u_1 + 1} (α := ℤ × M → M) ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (-x.1, x.2))
    ((fun (x : M) ↦ x⁻¹) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1)
⊢ Eq (α := M) (prod (map ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (-x.1, x.2)) l))
    (prod (map ((fun (x : M) ↦ x⁻¹) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) l))

Tactic:
congr! 2
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
h :
  ∀ (p : ℤ × M),
    Eq (α := M) (((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (-x.1, x.2)) p)
      (((fun (x : M) ↦ x⁻¹) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) p)
⊢ Eq.{u_1 + 1} (α := ℤ × M → M) ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (-x.1, x.2))
    ((fun (x : M) ↦ x⁻¹) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1)

Tactic:
ext p
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
p : ℤ × M
⊢ Eq (α := M) (((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (-x.1, x.2)) p)
    (((fun (x : M) ↦ x⁻¹) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) p)

Tactic:
simp [zpow'_neg]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_neg
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
⊢ 1 / l.eval = l⁻¹.eval

Tactic:
simp [eval_inv]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_inv
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
x : M
h : x = l.eval
rw : l.eval⁻¹ = l⁻¹.eval
rw₁ rw₂ : l.eval⁻¹ = l.eval⁻¹
⊢ x⁻¹ = l⁻¹.eval

Tactic:
rw [h, eval_inv]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_inv
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
r : ℤ
l : NF M
⊢ l ^ r =
    map
      (fun (x : ℤ × M) ↦
        match (motive := ℤ × M → ℤ × M) x with
        | (a, x) => (r * a, x))
      l

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
simp :
  Eq (α := M) (prod (map ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (r * x.1, x.2)) l))
    (prod (map ((fun (x : M) ↦ zpow' x r) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) l))
⊢ Eq (α := M)
    (prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        (l ^ r)))
    (zpow'
      (prod
        (map
          (fun (x : ℤ × M) ↦
            match (motive := ℤ × M → M) x with
            | (r, x) => zpow' x r)
          l))
      r)

Tactic:
simp only [zpow_apply, list_prod_zpow', map_map]

Premises used: Mathlib.Tactic.FieldSimp.NF.zpow_apply, List.map_map, Mathlib.Tactic.FieldSimp.list_prod_zpow'
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
h :
  Eq.{u_1 + 1} (α := ℤ × M → M) ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (r * x.1, x.2))
    ((fun (x : M) ↦ zpow' x r) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1)
⊢ Eq (α := M) (prod (map ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (r * x.1, x.2)) l))
    (prod (map ((fun (x : M) ↦ zpow' x r) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) l))

Tactic:
congr! 2