awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
have succ : ∀ (q : M) (h : p * q ∣ p * p ^ n), ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
Tactic: rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
succ : ∀ (q : M) (h : p * q ∣ p * p ^ n), ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
have succ₁ : ∀ (hno : q ∣ p ^ n), ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
Tactic: rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : p * q ∣ p * p ^ n
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
have h₁ : ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
Tactic: rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
have succ : ∀ (i : ℕ) (hi : i ≤ n) (hq : q ~ᵤ p ^ i), ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
Tactic: rcases h with ⟨i, hi, hq⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
have succ : p * p ^ i ~ᵤ p ^ (i + 1)
Tactic: refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p ^ (i + 1)
have succ : p * p ^ i ~ᵤ p * p ^ i
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
have succ : ∀ (i : ℕ) (hi : i ≤ n) (hq : q ~ᵤ p ^ i), ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
Tactic: obtain ⟨i, hi, hq⟩ := ih.mp hno
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
hp : Prime p
n : ℕ
⊢ q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
have zero : ∀ {q : M}, q ∣ HPow.hPow (β := ℕ) p 0 ↔ ∃ (i : ℕ), i ≤ 0 ∧ q ~ᵤ p ^ i
Tactic: induction n generalizing q with
  | zero =>
    simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
  | succ n ih =>
    refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
    rw [pow_succ'] at h
    rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
    · rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
      rcases h with ⟨i, hi, hq⟩
      refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
      rw [pow_succ']
    · obtain ⟨i, hi, hq⟩ := ih.mp hno
      exact ⟨i, hi.trans n.le_succ, hq⟩
Cleared hypotheses: q, n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
hp : Prime p
n : ℕ
zero : ∀ {q : M}, q ∣ HPow.hPow (β := ℕ) p 0 ↔ ∃ (i : ℕ), i ≤ 0 ∧ q ~ᵤ p ^ i
⊢ q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
have succ : ∀ (n : ℕ) (ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i) {q : M},
  q ∣ p ^ (n + 1) ↔ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
Tactic: induction n generalizing q with
  | zero =>
    simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
  | succ n ih =>
    refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
    rw [pow_succ'] at h
    rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
    · rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
      rcases h with ⟨i, hi, hq⟩
      refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
      rw [pow_succ']
    · obtain ⟨i, hi, hq⟩ := ih.mp hno
      exact ⟨i, hi.trans n.le_succ, hq⟩
Cleared hypotheses: q, n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
⊢ a * b = 0
have have : ∀ (this : Decidable (a = 0)), a * b = 0
Tactic: have : Decidable (a = 0) := Classical.propDecidable (a = 0)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ a * b = 0
have rw : 0 * b = 0
Tactic: rw [ha, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
rw : 0 * b = 0
⊢ a * b = 0
have rw₁ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [ha, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * b = 0
have rw : a * 0 = 0
Tactic: rw [h ha, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
rw : a * 0 = 0
⊢ a * b = 0
have rw₁ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [h ha, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
h : Eq.{u_1 + 1} (α := M₀) 0 1
a : M₀
⊢ a = 0
have rw : a * 1 = 0
Tactic: rw [← mul_one a, ← h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
h : Eq.{u_1 + 1} (α := M₀) 0 1
a : M₀
rw : a * 1 = 0
⊢ a = 0
have rw₁ : a * 0 = 0
Tactic: rw [← mul_one a, ← h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
h : Eq.{u_1 + 1} (α := M₀) 0 1
a : M₀
rw : a * 1 = 0
rw₁ : a * 0 = 0
⊢ a = 0
have rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [← mul_one a, ← h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ (x ^ n.succ) ^ N = 0
have rw : x ^ (n.succ * N) = 0
Tactic: rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
rw : x ^ (n.succ * N) = 0
⊢ (x ^ n.succ) ^ N = 0
have rw₁ : x ^ (n * N + N) = 0
Tactic: rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
rw : x ^ (n.succ * N) = 0
rw₁ : x ^ (n * N + N) = 0
⊢ (x ^ n.succ) ^ N = 0
have rw₂ : x ^ (n * N) * x ^ N = 0
Tactic: rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
rw : x ^ (n.succ * N) = 0
rw₁ : x ^ (n * N + N) = 0
rw₂ : x ^ (n * N) * x ^ N = 0
⊢ (x ^ n.succ) ^ N = 0
have rw₃ : x ^ (n * N) * 0 = 0
Tactic: rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
rw : x ^ (n.succ * N) = 0
rw₁ : x ^ (n * N + N) = 0
rw₂ : x ^ (n * N) * x ^ N = 0
rw₃ : x ^ (n * N) * 0 = 0
⊢ (x ^ n.succ) ^ N = 0
have rw₄ : Eq.{u_5 + 1} (α := S) 0 0
Tactic: rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
R : Type u_3
inst : MonoidWithZero R
x : R
m : ℕ
h_1 : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = 0
have rw : x ^ (m * n) = (x ^ m) ^ n
Tactic: rw [← h, pow_mul x m n]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
R : Type u_3
inst : MonoidWithZero R
x : R
m : ℕ
h_1 : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
rw : x ^ (m * n) = (x ^ m) ^ n
⊢ x ^ (m * n) = 0
have rw₁ : (x ^ m) ^ n = (x ^ m) ^ n
Tactic: rw [← h, pow_mul x m n]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : n ≠ 0
⊢ IsNilpotent (x ^ n)
have zero : ∀ (hn : Ne (α := ℕ) 0 0), IsNilpotent (HPow.hPow (β := ℕ) x 0)
Tactic: cases n with
  | zero => contradiction
  | succ => exact IsNilpotent.pow_succ _ hx
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), IsNilpotent (HPow.hPow (β := ℕ) x 0)
⊢ IsNilpotent (x ^ n)
have succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), IsNilpotent (x ^ (n + 1))
Tactic: cases n with
  | zero => contradiction
  | succ => exact IsNilpotent.pow_succ _ hx
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : n + 1 ≠ 0
⊢ HPow.hPow (α := M₀) 0 (n + 1) = 0
have rw : HPow.hPow (α := M₀) 0 n * 0 = 0
Tactic: rw [pow_succ, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : n + 1 ≠ 0
rw : HPow.hPow (α := M₀) 0 n * 0 = 0
⊢ HPow.hPow (α := M₀) 0 (n + 1) = 0
have rw₁ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [pow_succ, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
⊢ HPow.hPow (α := M₀) 0 n = if n = 0 then 1 else 0
have pos : ∀ (h : n = 0), HPow.hPow (α := M₀) 0 n = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
pos : ∀ (h : n = 0), HPow.hPow (α := M₀) 0 n = 1
⊢ HPow.hPow (α := M₀) 0 n = if n = 0 then 1 else 0
have neg : ∀ (h : ¬n = 0), HPow.hPow (α := M₀) 0 n = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : n = 0
⊢ HPow.hPow (α := M₀) 0 n = 1
have pos : HPow.hPow (α := M₀) (β := ℕ) 0 0 = 1
Tactic: rw [h, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : n = 0
pos : HPow.hPow (α := M₀) (β := ℕ) 0 0 = 1
⊢ HPow.hPow (α := M₀) 0 n = 1
have pos₁ : Eq.{u_1 + 1} (α := M₀) 1 1
Tactic: rw [h, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
⊢ HPow.hPow (α := M₀) 0 n = 0
have neg : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [zero_pow h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
inst_1 : Nontrivial M₀
⊢ HPow.hPow (α := M₀) 0 n = 1 ↔ n = 0
have rw : Eq.{u_1 + 1} (α := M₀) (if n = 0 then 1 else 0) 1 ↔ n = 0
Tactic: rw [zero_pow_eq, one_ne_zero.ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
inst_1 : Nontrivial M₀
rw : Eq.{u_1 + 1} (α := M₀) (if n = 0 then 1 else 0) 1 ↔ n = 0
⊢ HPow.hPow (α := M₀) 0 n = 1 ↔ n = 0
have rw₁ : n = 0 ↔ n = 0
Tactic: rw [zero_pow_eq, one_ne_zero.ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n m : ℕ
hmn : n.le m
ha : a ^ n = 0
⊢ a ^ m.succ = 0
have rw : a ^ m * a = 0
Tactic: rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n m : ℕ
hmn : n.le m
ha : a ^ n = 0
rw : a ^ m * a = 0
⊢ a ^ m.succ = 0
have rw₁ : 0 * a = 0
Tactic: rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n m : ℕ
hmn : n.le m
ha : a ^ n = 0
rw : a ^ m * a = 0
rw₁ : 0 * a = 0
⊢ a ^ m.succ = 0
have rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ n * b = 0
have rw : a ^ (n - m) * 0 = 0
Tactic: rw [show n = n - m + m by lia, pow_add, mul_assoc, h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (hypothesis)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : MonoidWithZero M₀
a_1 : M₀
n_1 : ℕ
inst_1 : NoZeroDivisors M₀
a : M₀
h : IsNilpotent a
n : ℕ
ih : ∀ (ha : a ^ n = 0), a = 0
ha : a ^ (n + 1) = 0
⊢ a = 0
have ha₁ : a ^ n = 0 ∨ a = 0
Tactic: rw [pow_succ, mul_eq_zero] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : MonoidWithZero M₀
a_1 : M₀
n_1 : ℕ
inst_1 : NoZeroDivisors M₀
a : M₀
h : IsNilpotent a
n : ℕ
ha : a ^ n = 0
⊢ a = 0
have zero : ∀ (ha : HPow.hPow (β := ℕ) a 0 = 0), a = 0
Tactic: induction n with
    | zero => simpa using congr_arg (a * ·) ha
    | succ n ih => rw [pow_succ, mul_eq_zero] at ha; exact ha.elim ih id
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : MonoidWithZero M₀
a_1 : M₀
n_1 : ℕ
inst_1 : NoZeroDivisors M₀
a : M₀
h : IsNilpotent a
n : ℕ
ha : a ^ n = 0
zero : ∀ (ha : HPow.hPow (β := ℕ) a 0 = 0), a = 0
⊢ a = 0
have succ : ∀ (n : ℕ) (ih : ∀ (ha : a ^ n = 0), a = 0) (ha : a ^ (n + 1) = 0), a = 0
Tactic: induction n with
    | zero => simpa using congr_arg (a * ·) ha
    | succ n ih => rw [pow_succ, mul_eq_zero] at ha; exact ha.elim ih id
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n : ℕ
inst_1 : IsReduced M₀
inst_2 : Nontrivial M₀
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
have inl : HPow.hPow (β := ℕ) a 0 = 0 ↔ a = 0 ∧ Ne (α := ℕ) 0 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n : ℕ
inst_1 : IsReduced M₀
inst_2 : Nontrivial M₀
inl : HPow.hPow (β := ℕ) a 0 = 0 ↔ a = 0 ∧ Ne (α := ℕ) 0 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
have inr : ∀ (hn : n ≠ 0), a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
⊢ ∃ (b : α), a * b = 1
have inl : Subsingleton α → ∃ (b : α), a * b = 1
Tactic: obtain _ | _ := subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
inl : Subsingleton α → ∃ (b : α), a * b = 1
⊢ ∃ (b : α), a * b = 1
have inr : Nontrivial α → ∃ (b : α), a * b = 1
Tactic: obtain _ | _ := subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Nontrivial α
⊢ ∃ (b : α), a * b = 1
have inr : ∀ (b : α) (hb : b * a = 1), ∃ (b : α), a * b = 1
Tactic: obtain ⟨b, hb⟩ := h a ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Nontrivial α
b : α
hb : b * a = 1
⊢ ∃ (b : α), a * b = 1
have inr : ∀ (c : α) (hc : c * b = 1), ∃ (b : α), a * b = 1
Tactic: obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ ∃ (b : α), a * b = 1
have inr : a * b = 1
Tactic: refine ⟨b, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| a * b
have rw : 1
Tactic: rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ a * b = 1
have conv_lhs : a * b = 1
Tactic: conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
conv_lhs : a * b = 1
⊢ a * b = 1
have inr : Eq.{u_3 + 1} (α := α) 1 1
Tactic: conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
⊢ a * b = a ↔ a * b = a * 1
have rw : a * b = a ↔ a * b = a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
⊢ a * b = b ↔ a * b = 1 * b
have rw : a * b = b ↔ a * b = b
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a * b = a ↔ b = 1
have rw : b = 1 ↔ a * b = a
Tactic: rw [Iff.comm, ← mul_right_inj' ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
ha : a ≠ 0
rw : b = 1 ↔ a * b = a
⊢ a * b = a ↔ b = 1
have rw₁ : a * b = a * 1 ↔ a * b = a
Tactic: rw [Iff.comm, ← mul_right_inj' ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
ha : a ≠ 0
rw : b = 1 ↔ a * b = a
rw₁ : a * b = a * 1 ↔ a * b = a
⊢ a * b = a ↔ b = 1
have rw₂ : a * b = a ↔ a * b = a
Tactic: rw [Iff.comm, ← mul_right_inj' ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
hb : b ≠ 0
⊢ a * b = b ↔ a = 1
have rw : a = 1 ↔ a * b = b
Tactic: rw [Iff.comm, ← mul_left_inj' hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
hb : b ≠ 0
rw : a = 1 ↔ a * b = b
⊢ a * b = b ↔ a = 1
have rw₁ : a * b = 1 * b ↔ a * b = b
Tactic: rw [Iff.comm, ← mul_left_inj' hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
hb : b ≠ 0
rw : a = 1 ↔ a * b = b
rw₁ : a * b = 1 * b ↔ a * b = b
⊢ a * b = b ↔ a = 1
have rw₂ : a * b = b ↔ a * b = b
Tactic: rw [Iff.comm, ← mul_left_inj' hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a = a * b ↔ b = 1
have rw : a * b = a ↔ b = 1
Tactic: rw [eq_comm, mul_eq_left₀ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
ha : a ≠ 0
rw : a * b = a ↔ b = 1
⊢ a = a * b ↔ b = 1
have rw₁ : b = 1 ↔ b = 1
Tactic: rw [eq_comm, mul_eq_left₀ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
hb : b ≠ 0
⊢ b = a * b ↔ a = 1
have rw : a * b = b ↔ a = 1
Tactic: rw [eq_comm, mul_eq_right₀ hb]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
hb : b ≠ 0
rw : a * b = b ↔ a = 1
⊢ b = a * b ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [eq_comm, mul_eq_right₀ hb]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
h : a * b = 1
⊢ a⁻¹ = b
have rw : a⁻¹ = a⁻¹ * (a * b)
Tactic: rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
h : a * b = 1
rw : a⁻¹ = a⁻¹ * (a * b)
⊢ a⁻¹ = b
have rw₁ : a⁻¹ = a⁻¹ * 1
Tactic: rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
h : a * b = 1
rw : a⁻¹ = a⁻¹ * (a * b)
rw₁ : a⁻¹ = a⁻¹ * 1
⊢ a⁻¹ = b
have rw₂ : a⁻¹ = a⁻¹
Tactic: rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b x a : G₀
⊢ a⁻¹⁻¹ = a
have pos : ∀ (h : a = 0), a⁻¹⁻¹ = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b x a : G₀
pos : ∀ (h : a = 0), a⁻¹⁻¹ = a
⊢ a⁻¹⁻¹ = a
have neg : ∀ (h : ¬a = 0), a⁻¹⁻¹ = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have pos : ∀ (ha : a = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
pos : ∀ (ha : a = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have neg : ∀ (ha : ¬a = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : ¬a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have pos : ∀ (hb : b = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : ¬a = 0
pos : ∀ (hb : b = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have neg : ∀ (hb : ¬b = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have neg : a * b * (b⁻¹ * a⁻¹) = 1
Tactic: apply inv_eq_of_mul