awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ Ne (α := M)
    (prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)))
    0
have apply : Ne.{u_1 + 1} (α := M)
  ((fun (x : ℤ × M) ↦
      (match (motive := ℤ × M → M) x with
        | (r, x) => zpow' x r :
        M))
    (r, x))
  0
Tactic: apply mul_ne_zero ?_ hl
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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 < ((r, x) ::ᵣ l).eval
have unfold : LT.lt (α := M) 0
  (prod
    (map
      (fun (x : ℤ × M) ↦
        match (motive := ℤ × M → M) x with
        | (r, x) => zpow' x r)
      ((r, x) :: l)))
Tactic: unfold eval cons
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ LT.lt (α := M) 0
    (prod
      (map
        (fun (x : ℤ × M) ↦
          match (motive := ℤ × M → M) x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)))
have apply : LT.lt.{u_1} (α := M) 0
  ((fun (x : ℤ × M) ↦
      (match (motive := ℤ × M → M) x with
        | (r, x) => zpow' x r :
        M))
    (r, x))
Tactic: apply mul_pos ?_ hl
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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 < zpow' x r
have rw : 0 < x ^ r
Tactic: rw [zpow'_of_ne_zero_left _ _ hx.ne']
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
have 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
Tactic: simp only [eval_cons, ← h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : 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
have simp : l₁.eval * zpow' x r₁ * (l₂.eval * zpow' x r₂) = l₁.eval * l₂.eval * (zpow' x r₁ * zpow' x r₂)
Tactic: simp only [eval_cons, ← h, zpow'_add]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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₂ ::ᵣ l).eval
have 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
Tactic: simp only [eval_cons, ← h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ x₁ * x₂ = l.eval
have rw : l₁.eval * x₂ = l.eval
Tactic: rw [hx₁, hx₂, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ x₁ * x₂ = l.eval
have rw₂ : l.eval = l.eval
Tactic: rw [hx₁, hx₂, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
have 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
Tactic: simp only [eval_cons, ← h, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : 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
have simp : l₁.eval * zpow' x r₁ * (l₂.eval⁻¹ * zpow' x (-r₂)) = l₁.eval * l₂.eval⁻¹ * (zpow' x r₁ * zpow' x (-r₂))
Tactic: simp only [← h, eval_cons, div_eq_mul_inv, mul_inv, ← zpow'_neg, sub_eq_add_neg, zpow'_add]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ x₁ / x₂ = l.eval
have rw : l₁.eval / x₂ = l.eval
Tactic: rw [hx₁, hx₂, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ x₁ / x₂ = l.eval
have rw₂ : l.eval = l.eval
Tactic: rw [hx₁, hx₂, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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 * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval
have rw : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = ((n, e) ::ᵣ l').eval
Tactic: rw [eval_cons, eval_cons, ← h, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval
have rw₁ : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = l'.eval * zpow' (n, e).2 (n, e).1
Tactic: rw [eval_cons, eval_cons, ← h, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval
have rw₂ : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = L.eval * l.eval * zpow' (n, e).2 (n, e).1
Tactic: rw [eval_cons, eval_cons, ← h, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval
have rw₃ : L.eval * (l.eval * zpow' (n, e).2 (n, e).1) = L.eval * (l.eval * zpow' (n, e).2 (n, e).1)
Tactic: rw [eval_cons, eval_cons, ← h, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ L.eval * l₀.eval = ((0, e) ::ᵣ l').eval
have rw : L.eval * l₀.eval = L.eval * ((0, e) ::ᵣ l).eval
Tactic: rw [← eval_mul_eval_cons 0 e h, h']
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ L.eval * l₀.eval = ((0, e) ::ᵣ l').eval
have rw₁ : L.eval * l₀.eval = L.eval * l₀.eval
Tactic: rw [← eval_mul_eval_cons 0 e h, h']
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : 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
have rw : L.eval * zpow' (n, e).2 (n, e).1 * l.eval = L.eval * l.eval * zpow' (n, e).2 (n, e).1
Tactic: rw [eval_cons, eval_cons, ← h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval
have rw : ((n + -n, e) ::ᵣ l').eval = l'.eval
Tactic: rw [mul_eq_eval₂ n (-n) e h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ ((n, e) ::ᵣ t).eval = ((n, e) ::ᵣ t_n).eval / t_d.eval
have simp : t_n.eval * t_d.eval⁻¹ * zpow' e n = t_n.eval * zpow' e n * t_d.eval⁻¹
Tactic: simp only [eval_cons, h, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ ((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval
have simp : t_n.eval * t_d.eval⁻¹ * (zpow' e n)⁻¹ = t_n.eval * (t_d.eval⁻¹ * (zpow' e n)⁻¹)
Tactic: simp only [eval_cons, h, zpow'_neg, div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
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
⊢ ((0, e) ::ᵣ t).eval = ((1, e) ::ᵣ t_n).eval / ((1, e) ::ᵣ t_d).eval
have 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))
Tactic: simp only [eval_cons, h, div_eq_mul_inv, mul_inv, ← zpow'_neg, ← add_neg_cancel (1:ℤ), zpow'_add]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
⊢ l⁻¹.eval = l.eval⁻¹
have 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))
Tactic: simp +instances only [NF.eval, List.map_map, NF.instInv, List.prod_inv]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
⊢ 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))
have 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)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
⊢ 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)
have 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)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
x : M
h : x = l.eval
⊢ x⁻¹ = l⁻¹.eval
have rw : l.eval⁻¹ = l⁻¹.eval
Tactic: rw [h, eval_inv]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
x : M
h : x = l.eval
rw : l.eval⁻¹ = l⁻¹.eval
⊢ x⁻¹ = l⁻¹.eval
have rw₁ : l.eval⁻¹ = l.eval⁻¹
Tactic: rw [h, eval_inv]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
⊢ 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)
have 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))
Tactic: simp only [zpow_apply, list_prod_zpow', map_map]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
⊢ 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))
have 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)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
⊢ 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)
have h : ∀ (p : ℤ × M),
  Eq (α := M) (((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (r * x.1, x.2)) p)
    (((fun (x : M) ↦ zpow' x r) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) p)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval
have rw : zpow' x r = (l ^ r).eval
Tactic: rw [← zpow'_of_ne_zero_right x r hr, eval_zpow', hx]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
rw : zpow' x r = (l ^ r).eval
⊢ x ^ r = (l ^ r).eval
have rw₁ : zpow' x r = zpow' l.eval r
Tactic: rw [← zpow'_of_ne_zero_right x r hr, eval_zpow', hx]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
rw : zpow' x r = (l ^ r).eval
rw₁ : zpow' x r = zpow' l.eval r
⊢ x ^ r = (l ^ r).eval
have rw₂ : zpow' l.eval r = zpow' l.eval r
Tactic: rw [← zpow'_of_ne_zero_right x r hr, eval_zpow', hx]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval
have rw : l.eval ^ r = zpow' l.eval (↑r : ℤ)
Tactic: rw [eval_pow, hx]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ l.eval ^ r = zpow' l.eval (↑r : ℤ)
have rw : l.eval ^ r = l.eval ^ r
Tactic: rw [zpow'_ofNat _ hr]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : 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
have rw : ((r, x) ::ᵣ t).eval = ((r, x) ::ᵣ t').eval
Tactic: rw [← h', eval_cons, eval_cons, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
rw : ((r, x) ::ᵣ t).eval = ((r, x) ::ᵣ t').eval
⊢ ((r, x) ::ᵣ t).eval = l'.eval
have rw₁ : t.eval * zpow' (r, x).2 (r, x).1 = ((r, x) ::ᵣ t').eval
Tactic: rw [← h', eval_cons, eval_cons, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
rw : ((r, x) ::ᵣ t).eval = ((r, x) ::ᵣ t').eval
rw₁ : t.eval * zpow' (r, x).2 (r, x).1 = ((r, x) ::ᵣ t').eval
⊢ ((r, x) ::ᵣ t).eval = l'.eval
have rw₂ : t.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1
Tactic: rw [← h', eval_cons, eval_cons, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp.Lemmas (goal)
Goal:
M : Type u_1
inst : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
rw : ((r, x) ::ᵣ t).eval = ((r, x) ::ᵣ t').eval
rw₁ : t.eval * zpow' (r, x).2 (r, x).1 = ((r, x) ::ᵣ t').eval
rw₂ : t.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1
⊢ ((r, x) ::ᵣ t).eval = l'.eval
have rw₃ : t'.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1
Tactic: rw [← h', eval_cons, eval_cons, h]
-- Lean 4 proof step from Mathlib.Tactic.FieldSimp (goal)
Goal:
«$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
«$snd» : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ ((«$r», «$x») ::ᵣ []).eval = «$e»
have rw : NF.eval [] * zpow' («$r», «$x»).2 («$r», «$x»).1 = «$e»
Tactic: rw [NF.eval_cons]
-- Lean 4 proof step from Mathlib.Tactic.Group (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
n m : ℤ
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)
have rw : a * (b ^ n * b ^ m) = a * b ^ (n + m)
Tactic: rw [mul_assoc, ← zpow_add]
-- Lean 4 proof step from Mathlib.Tactic.Group (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
n m : ℤ
rw : a * (b ^ n * b ^ m) = a * b ^ (n + m)
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)
have rw₁ : a * b ^ (n + m) = a * b ^ (n + m)
Tactic: rw [mul_assoc, ← zpow_add]
-- Lean 4 proof step from Mathlib.Tactic.Group (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
m : ℤ
⊢ a * b * b ^ m = a * b ^ (m + 1)
have rw : a * (b * b ^ m) = a * b ^ (m + 1)
Tactic: rw [mul_assoc, mul_self_zpow]
-- Lean 4 proof step from Mathlib.Tactic.Group (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
m : ℤ
rw : a * (b * b ^ m) = a * b ^ (m + 1)
⊢ a * b * b ^ m = a * b ^ (m + 1)
have rw₁ : a * b ^ (m + 1) = a * b ^ (m + 1)
Tactic: rw [mul_assoc, mul_self_zpow]
-- Lean 4 proof step from Mathlib.Tactic.Group (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
n : ℤ
⊢ a * b ^ n * b = a * b ^ (n + 1)
have rw : a * (b ^ n * b) = a * b ^ (n + 1)
Tactic: rw [mul_assoc, mul_zpow_self]
-- Lean 4 proof step from Mathlib.Tactic.Group (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
n : ℤ
rw : a * (b ^ n * b) = a * b ^ (n + 1)
⊢ a * b ^ n * b = a * b ^ (n + 1)
have rw₁ : a * b ^ (n + 1) = a * b ^ (n + 1)
Tactic: rw [mul_assoc, mul_zpow_self]
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
p q : IProp
⊢ Ordering
have var : Nat → Ordering
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
p q : IProp
var : Nat → Ordering
true false : Ordering
⊢ Ordering
have and' : AndKind → IProp → IProp → Ordering
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
a : Nat
⊢ Ordering
have var : Nat → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
a : Nat
var : Nat → Ordering
var₁ var₂ : Ordering
⊢ Ordering
have var₃ : AndKind → IProp → IProp → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
⊢ Ordering
have true : Nat → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
true : Nat → Ordering
cases true₁ : Ordering
⊢ Ordering
have true₂ : AndKind → IProp → IProp → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
⊢ Ordering
have false : Nat → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
false : Nat → Ordering
false₁ cases : Ordering
⊢ Ordering
have false₂ : AndKind → IProp → IProp → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
a : AndKind
a_1 a_2 : IProp
⊢ Ordering
have and' : Nat → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q : IProp
a : AndKind
a_1 a_2 : IProp
and' : Nat → Ordering
and'₁ and'₂ : Ordering
⊢ Ordering
have and'₃ : AndKind → IProp → IProp → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q a a_1 : IProp
⊢ Ordering
have or : Nat → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q a a_1 : IProp
or : Nat → Ordering
or₁ or₂ : Ordering
⊢ Ordering
have or₃ : AndKind → IProp → IProp → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q a a_1 : IProp
⊢ Ordering
have imp : Nat → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.ITauto (goal)
Goal:
q a a_1 : IProp
imp : Nat → Ordering
imp₁ imp₂ : Ordering
⊢ Ordering
have imp₃ : AndKind → IProp → IProp → Ordering
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Tactic.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst : CanLift α β coeβα condβα
inst_1 : CanLift γ δ coeδγ condδγ
x : α
y : γ
hx : condβα (x, y).fst
hy : condδγ (x, y).snd
⊢ ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (x, y)
have rcases : ∀ (x : β) (hx : condβα (coeβα x, y).fst) (hy : condδγ (coeβα x, y).snd),
  ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (coeβα x, y)
Tactic: rcases CanLift.prf (β := β) x hx with ⟨x, rfl⟩
Cleared hypotheses: x, hx, hy
-- Lean 4 proof step from Mathlib.Tactic.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst : CanLift α β coeβα condβα
inst_1 : CanLift γ δ coeδγ condδγ
y : γ
x : β
hx : condβα (coeβα x, y).fst
hy : condδγ (coeβα x, y).snd
⊢ ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (coeβα x, y)
have rcases : ∀ (y : δ) (hx : condβα (coeβα x, coeδγ y).fst) (hy : condδγ (coeβα x, coeδγ y).snd),
  ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (coeβα x, coeδγ y)
Tactic: rcases CanLift.prf (β := δ) y hy with ⟨y, rfl⟩
Cleared hypotheses: y, hx, hy
-- Lean 4 proof step from Mathlib.Tactic.Lift (goal)
Goal:
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty.{u_2} (α i)
p : ι → Prop
f : (i : Subtype p) → α (i.val (p := p))
⊢ ∃ (g : (i : ι) → α i), (fun (i : Subtype p) ↦ g (i.val (p := p))) = f
have haveI : ∀ (this : DecidablePred p), ∃ (g : (i : ι) → α i), (fun (i : Subtype p) ↦ g (i.val (p := p))) = f
Tactic: haveI : DecidablePred p := fun i ↦ Classical.propDecidable (p i)
-- Lean 4 proof step from Mathlib.Tactic.Linarith.Preprocessing (goal)
Goal:
M : Type u_1
inst : MulOneClass M
a b : M
h : 1 * a = b
⊢ a = b
have rwa : ∀ (h : a = b), a = b
Tactic: rwa [one_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (hypothesis)
Goal:
α : Type u_1
a a' b b' : α
inst : Add α
inst_1 : IsRightCancelAdd α
p : a = b
H : a' + b = b' + a
⊢ a' = b'
have H₁ : a' + b = b' + b
Tactic: rw [p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ a' ≤ b'
have grw : a' + b ≤ b' + b
Tactic: grw [← add_le_add_iff_right b, H, p]
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
grw : a' + b ≤ b' + b
⊢ a' ≤ b'
have grw₁ : b' + a ≤ b' + b
Tactic: grw [← add_le_add_iff_right b, H, p]
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
grw : a' + b ≤ b' + b
grw₁ : b' + a ≤ b' + b
⊢ a' ≤ b'
have grw₂ : b' + b ≤ b' + b
Tactic: grw [← add_le_add_iff_right b, H, p]
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a = b
H : a' + b ≤ b' + a
⊢ a' ≤ b'
have rwa : ∀ (H : a' + b ≤ b' + b), a' ≤ b'
Tactic: rwa [p, add_le_add_iff_right] at H
Cleared hypotheses: H