awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 ∧ q ~ᵤ p ^ i

Tactic:
rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h

Premises used: mul_dvd_mul_iff_left, Prime.ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
succ : ∀ (i : ℕ) (hi : i ≤ n) (hq : q ~ᵤ p ^ i), ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Tactic:
rcases h with ⟨i, hi, hq⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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

Tactic:
⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩

Premises used: Associated.trans, HAdd.hAdd, And.intro, Exists.intro, Associated.mul_left, OfNat.ofNat, Nat.succ_le_succ
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
succ : p * p ^ i ~ᵤ p ^ (i + 1)
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Tactic:
refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
succ succ₁ : p * p ^ i ~ᵤ p * p ^ i
⊢ p * p ^ i ~ᵤ p ^ (i + 1)

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
succ : ∀ (i : ℕ) (hi : i ≤ n) (hq : q ~ᵤ p ^ i), ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
obtain ⟨i, hi, hq⟩ := ih.mp hno

Premises used: Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
⟨i, hi.trans n.le_succ, hq⟩

Premises used: Nat.le_succ, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
exact ⟨i, hi.trans n.le_succ, hq⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
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
⊢ q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ 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⟩

Premises used: associated_one_iff_isUnit, mul_dvd_mul_iff_left, Prime.ne_zero, isUnit_iff_dvd_one, pow_succ', rfl
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
⊢ a * b ≠ 0 → a ≠ 0

Tactic:
mt fun h => mul_eq_zero_of_left h b

Premises used: mt, mul_eq_zero_of_left
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
⊢ a * b ≠ 0 → b ≠ 0

Tactic:
mt (mul_eq_zero_of_right a)

Premises used: mul_eq_zero_of_right, mt
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a * b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
⟨left_ne_zero_of_mul h, right_ne_zero_of_mul h⟩

Premises used: right_ne_zero_of_mul, And.intro, left_ne_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
have : ∀ (this : Decidable (a = 0)), a * b = 0
⊢ a * b = 0

Tactic:
have : Decidable (a = 0) := Classical.propDecidable (a = 0)
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ a * b = 0

Tactic:
rw [ha, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ a * b = 0

Tactic:
rw [h ha, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
⊢ a * b = 0

Tactic:
exact if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ Eq (α := M₀ → M₀) (fun (x : M₀) ↦ 0 * x) (const M₀ 0)

Tactic:
funext zero_mul

Premises used: MulZeroClass.zero_mul, funext
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ Eq (α := M₀ → M₀) (fun (x : M₀) ↦ x * 0) (const M₀ 0)

Tactic:
funext mul_zero

Premises used: MulZeroClass.mul_zero, funext
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : NoZeroDivisors M₀
a : M₀
h : a * a = 0
⊢ a = 0

Tactic:
(eq_zero_or_eq_zero_of_mul_eq_zero h).elim id id

Premises used: id, Or.elim, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b ≠ 0

Tactic:
mt eq_zero_or_eq_zero_of_mul_eq_zero <| not_or.mpr ⟨ha, hb⟩

Premises used: Iff.mpr, mt, not_or, And.intro, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : Zero M₀
inst_1 : Mul M₀
inst_2 : NoZeroDivisors M₀
x y : M₀
inst_3 : NeZero x
inst_4 : NeZero y
⊢ NeZero (x * y)

Tactic:
⟨mul_ne_zero out out⟩

Premises used: NeZero.mk, NeZero.out, mul_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ a = 0

Tactic:
rw [← mul_one a, ← h, mul_zero]

Premises used: MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
⊢ Eq.{u_1 + 1} (α := M₀) 0 1 ↔ Subsingleton M₀

Tactic:
⟨fun h => haveI := uniqueOfZeroEqOne h; inferInstance, fun h => @Subsingleton.elim _ h _ _⟩

Premises used: inferInstance, Iff.intro, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
h : Eq.{u_1 + 1} (α := M₀) 0 1
a b : M₀
⊢ a = b

Tactic:
@Subsingleton.elim _ (subsingleton_of_zero_eq_one h) a b

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
⊢ Ne.{u_1 + 1} (α := M₀) 0 1 ∨ ∀ (a : M₀), a = 0

Tactic:
not_or_of_imp eq_zero_of_zero_eq_one

Premises used: eq_zero_of_zero_eq_one, not_or_of_imp
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
a b : M₀
h : a * b = 1
⊢ a ≠ 0

Tactic:
left_ne_zero_of_mul <| ne_zero_of_eq_one h

Premises used: ne_zero_of_eq_one, left_ne_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
a b : M₀
h : a * b = 1
⊢ b ≠ 0

Tactic:
right_ne_zero_of_mul <| ne_zero_of_eq_one h

Premises used: ne_zero_of_eq_one, right_ne_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_3
inst : Zero R
inst_1 : Pow R ℕ
x : R
n : ℕ
e : x ^ n = 0
⊢ IsNilpotent x

Tactic:
⟨n, e⟩

Premises used: Exists.intro, IsNilpotent
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_3
x : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : Subsingleton R
⊢ IsNilpotent x

Tactic:
⟨0, Subsingleton.elim _ _⟩

Premises used: Exists.intro, Subsingleton.elim, OfNat.ofNat, IsNilpotent
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_3
inst : MonoidWithZero R
⊢ IsNilpotent.{u_3} (R := R) 0

Tactic:
⟨1, pow_one 0⟩

Premises used: pow_one, Exists.intro, OfNat.ofNat, IsNilpotent
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_3
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ ¬IsNilpotent.{u_3} (R := R) 1

Tactic:
fun ⟨_, H⟩ ↦ zero_ne_one (H.symm.trans (one_pow _))

Premises used: one_pow, False, zero_ne_one, _private.0.not_isNilpotent_one.match_1, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₄ rw₅ : Eq.{u_5 + 1} (α := S) 0 0
⊢ (x ^ n.succ) ^ N = 0

Tactic:
rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]

Premises used: pow_add, pow_mul, MulZeroClass.mul_zero, Nat.succ_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₁ rw₂ : (x ^ m) ^ n = (x ^ m) ^ n
⊢ x ^ (m * n) = 0

Tactic:
rw [← h, pow_mul x m n]

Premises used: pow_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : Ne (α := ℕ) 0 0
⊢ IsNilpotent (HPow.hPow (β := ℕ) x 0)

Tactic:
contradiction
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
n : ℕ
hn : n + 1 ≠ 0
⊢ IsNilpotent (x ^ (n + 1))

Tactic:
IsNilpotent.pow_succ _ hx

Premises used: IsNilpotent.pow_succ
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
S : Type u_5
inst : MonoidWithZero S
x : S
hx : IsNilpotent x
n : ℕ
hn : n + 1 ≠ 0
⊢ IsNilpotent (x ^ (n + 1))

Tactic:
exact IsNilpotent.pow_succ _ hx

Premises used: IsNilpotent.pow_succ
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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)
succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), IsNilpotent (x ^ (n + 1))
⊢ IsNilpotent (x ^ n)

Tactic:
cases n with
  | zero => contradiction
  | succ => exact IsNilpotent.pow_succ _ hx

Premises used: IsNilpotent.pow_succ, IsNilpotent.zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
n : ℕ
S : Type u_5
inst : MonoidWithZero S
x : S
hn : n ≠ 0
⊢ IsNilpotent (x ^ n) ↔ IsNilpotent x

Tactic:
⟨of_pow, (pow_of_pos · hn)⟩

Premises used: Iff.intro, IsNilpotent.pow_of_pos, IsNilpotent.of_pow
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_3
x : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : IsReduced R
n : ℕ
h : x ^ n = 0
⊢ x = 0

Tactic:
IsReduced.eq_zero x ⟨n, h⟩

Premises used: Exists.intro, IsReduced.eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
R : Type u_3
S : Type u_4
x y : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : Subsingleton R
⊢ IsReduced R

Tactic:
⟨fun _ _ => Subsingleton.elim ..⟩

Premises used: IsReduced.mk, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_3
x : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : IsReduced R
h : IsNilpotent x
⊢ x = 0

Tactic:
IsReduced.eq_zero x h

Premises used: IsReduced.eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_3
x : R
inst : MonoidWithZero R
inst_1 : IsReduced R
⊢ IsNilpotent x ↔ x = 0

Tactic:
⟨fun h => h.eq_zero, fun h => h.symm ▸ IsNilpotent.zero⟩

Premises used: Eq.rec, Iff.intro, IsNilpotent.eq_zero, Eq.symm, IsNilpotent.zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
R : Type u_5
inst : Zero R
inst_1 : Pow R ℕ
h : ¬IsReduced R
⊢ ∃ (x : R), x ≠ 0 ∧ IsNilpotent x

Tactic:
simpa [isReduced_iff, not_forall, and_comm] using h

Premises used: isReduced_iff, and_comm, Classical.not_forall
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : n + 1 ≠ 0
rw : HPow.hPow (α := M₀) 0 n * 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ HPow.hPow (α := M₀) 0 (n + 1) = 0

Tactic:
rw [pow_succ, mul_zero]

Premises used: pow_succ, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
pos : ∀ (h : n = 0), HPow.hPow (α := M₀) 0 n = 1
neg : ∀ (h : ¬n = 0), HPow.hPow (α := M₀) 0 n = 0
⊢ HPow.hPow (α := M₀) 0 n = if n = 0 then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : n = 0
pos : HPow.hPow (α := M₀) (β := ℕ) 0 0 = 1
pos₁ pos₂ : Eq.{u_1 + 1} (α := M₀) 1 1
⊢ HPow.hPow (α := M₀) 0 n = 1

Tactic:
rw [h, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
neg neg₁ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ HPow.hPow (α := M₀) 0 n = 0

Tactic:
rw [zero_pow h]

Premises used: zero_pow
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₁ rw₂ : n = 0 ↔ n = 0
⊢ HPow.hPow (α := M₀) 0 n = 1 ↔ n = 0

Tactic:
rw [zero_pow_eq, one_ne_zero.ite_eq_left_iff]

Premises used: Ne.ite_eq_left_iff, zero_pow_eq, one_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ a ^ m.succ = 0

Tactic:
rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]

Premises used: pow_succ, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
hn : n ≠ 0
ha : HPow.hPow (α := M₀) 0 n ≠ 0
⊢ False

Tactic:
ha <| zero_pow hn

Premises used: zero_pow
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
n : ℕ
hn : n ≠ 0
ha : HPow.hPow (α := M₀) 0 n ≠ 0
⊢ False

Tactic:
exact ha <| zero_pow hn

Premises used: zero_pow
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
h : HPow.hPow (α := M₀) (β := ℕ) 0 0 = 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ n = n - m + m

Tactic:
lia
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
rw : a ^ (n - m) * 0 = 0
⊢ a ^ n * b = 0

Tactic:
rw [show n = n - m + m by lia, pow_add, mul_assoc, h]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ (n - m) * 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : MonoidWithZero M₀
a_1 : M₀
n : ℕ
inst_1 : NoZeroDivisors M₀
a : M₀
h : IsNilpotent a
ha : HPow.hPow (β := ℕ) a 0 = 0
⊢ a = 0

Tactic:
simpa using congr_arg (a * ·) ha

Premises used: HMul.hMul, congr_arg
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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 ^ n = 0 ∨ a = 0

Tactic:
rw [pow_succ, mul_eq_zero] at ha

Premises used: pow_succ, mul_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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 = 0 ∨ a = 0
⊢ a = 0

Tactic:
ha.elim ih id

Premises used: id, Or.elim
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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 = 0 ∨ a = 0
⊢ a = 0

Tactic:
exact ha.elim ih id

Premises used: id, Or.elim
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
succ : ∀ (n : ℕ) (ih : ∀ (ha : a ^ n = 0), a = 0) (ha : a ^ (n + 1) = 0), a = 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

Premises used: HMul.hMul, pow_succ, mul_eq_zero, congr_arg
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n : ℕ
inst_1 : IsReduced M₀
hn : n ≠ 0
⊢ a ^ n = 0 ↔ a = 0

Tactic:
⟨eq_zero_of_pow_eq_zero, (·.symm ▸ zero_pow hn)⟩

Premises used: Eq.rec, Iff.intro, eq_zero_of_pow_eq_zero, Eq.symm, zero_pow
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n : ℕ
inst_1 : IsReduced M₀
hn : n ≠ 0
⊢ a ^ n ≠ 0 ↔ a ≠ 0

Tactic:
(pow_eq_zero_iff hn).not

Premises used: pow_eq_zero_iff, Iff.not
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
inst_1 : IsReduced M₀
n : ℕ
h : a ≠ 0
⊢ a ^ n ≠ 0

Tactic:
mt eq_zero_of_pow_eq_zero h

Premises used: mt, eq_zero_of_pow_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
n : ℕ
inst_1 : IsReduced M₀
inst_2 : NeZero a
⊢ NeZero (a ^ n)

Tactic:
⟨pow_ne_zero n NeZero.out⟩

Premises used: NeZero.mk, pow_ne_zero, NeZero.out
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
inst_1 : IsReduced M₀
⊢ HPow.hPow (β := ℕ) a 2 = 0 ↔ a = 0

Tactic:
pow_eq_zero_iff two_ne_zero

Premises used: pow_eq_zero_iff, two_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
inr : ∀ (hn : n ≠ 0), a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
inst_1 : IsReduced M₀
inst_2 : Nontrivial M₀
⊢ HPow.hPow (β := ℕ) a 0 = 0 ↔ a = 0 ∧ Ne (α := ℕ) 0 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a : M₀
n : ℕ
inst_1 : IsReduced M₀
inst_2 : Nontrivial M₀
hn : n ≠ 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
inl : Subsingleton α → ∃ (b : α), a * b = 1
inr : Nontrivial α → ∃ (b : α), a * b = 1
⊢ ∃ (b : α), a * b = 1

Tactic:
obtain _ | _ := subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Subsingleton α
⊢ ∃ (b : α), a * b = 1

Tactic:
⟨a, Subsingleton.elim _ _⟩

Premises used: Exists.intro, Subsingleton.elim
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Subsingleton α
⊢ ∃ (b : α), a * b = 1

Tactic:
exact ⟨a, Subsingleton.elim _ _⟩
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
α : Type u_3
inst : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1
a : α
ha : a ≠ 0
h_1 : Nontrivial α
inr : ∀ (b : α) (hb : b * a = 1), ∃ (b : α), a * b = 1
⊢ ∃ (b : α), a * b = 1

Tactic:
obtain ⟨b, hb⟩ := h a ha
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
inr : ∀ (c : α) (hc : c * b = 1), ∃ (b : α), a * b = 1
⊢ ∃ (b : α), a * b = 1

Tactic:
obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)

Premises used: left_ne_zero_of_mul, Eq.trans_ne, one_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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

Tactic:
⟨b, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
inr : a * b = 1
⊢ ∃ (b : α), a * b = 1

Tactic:
refine ⟨b, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw : 1
| a * b

Tactic:
rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]

Premises used: HMul.hMul, mul_assoc, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
inr : Eq.{u_3 + 1} (α := α) 1 1
⊢ a * b = 1

Tactic:
conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]

Premises used: HMul.hMul, mul_assoc, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
rw rw₁ : a * b = a ↔ a * b = a
⊢ a * b = a ↔ a * b = a * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
rw rw₁ : a * b = b ↔ a * b = b
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₂ rw₃ : a * b = a ↔ a * b = a
⊢ a * b = a ↔ b = 1

Tactic:
rw [Iff.comm, ← mul_right_inj' ha, mul_one]

Premises used: Iff.comm, mul_right_inj', mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₂ rw₃ : a * b = b ↔ a * b = b
⊢ a * b = b ↔ a = 1

Tactic:
rw [Iff.comm, ← mul_left_inj' hb, one_mul]

Premises used: Iff.comm, mul_left_inj', one_mul