awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
none :
  Eq.{u_2 + 1} (α := ValueGroup₀ f) Option.none 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      Eq (α := ValueGroup₀ f) Option.none (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
⊢ x = 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      x = (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
have some : ∀ (x : Bˣ) (hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x),
  some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx) = 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx) =
        (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
Tactic: obtain _ | ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f) none 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      Eq (α := ValueGroup₀ f) none (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
have none : Eq.{u_2 + 1} (α := ValueGroup₀ f) none 0
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (hypothesis)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
⊢ some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx) = 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx) =
        (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
have hx₁ : ∃ (a : A),
  Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
    ∃ (x_1 : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x_1 : B) (0 : B) ∧
        HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑x : B) = (f : (a : A) → B) x_1
Tactic: rw [mem_valueGroup_iff_of_comm'] at hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx_1 : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
hx :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x_1 : A),
        Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x_1 : B) (0 : B) ∧
          HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑x : B) = (f : (a : A) → B) x_1
⊢ some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) = 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) =
        (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
have some : ∀ (r : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (s : A)
  (hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B))
  (hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s),
  some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) = 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) =
        (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
Tactic: obtain ⟨r, hr, s, hs, hrs⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
r : A
hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)
s : A
hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)
hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s
⊢ Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx = valueGroup.mk f r s hr hs
have simp : x =
  HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r) hr)⁻¹ : Bˣ) (Units.mk0 ((f : (a : A) → B) s) hs : Bˣ)
Tactic: simp only [valueGroup.mk, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
r : A
hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)
s : A
hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)
hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s
⊢ x =
    HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r) hr)⁻¹ : Bˣ)
      (Units.mk0 ((f : (a : A) → B) s) hs : Bˣ)
have rw : HMul.hMul (α := Bˣ) (Units.mk0 ((f : (a : A) → B) r) hr : Bˣ) x = Units.mk0 ((f : (a : A) → B) s) hs
Tactic: rw [eq_inv_mul_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ ¬IsLeftRegular.{u_1} (R := R) 0 ↔ Nontrivial R
have rw : (¬∃ (x : R), ∃ (y : R), x ≠ y) ↔ ∀ (x y : R), x = y
Tactic: rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ (¬∃ (x : R), ∃ (y : R), x ≠ y) ↔ ∀ (x y : R), x = y
have push : (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ ¬IsRightRegular.{u_1} (R := R) 0 ↔ Nontrivial R
have rw : (¬∃ (x : R), ∃ (y : R), x ≠ y) ↔ ∀ (x y : R), x = y
Tactic: rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
la : IsLeftRegular.{u_1} (R := R) 0
⊢ False
have rcases : ∀ (x y : R) (xy : x ≠ y), False
Tactic: rcases exists_pair_ne R with ⟨x, y, xy⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
la : IsLeftRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
⊢ False
have refine : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ 0 * x) x) ((fun (x : R) ↦ 0 * x) y)
Tactic: refine xy (la ?_)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
ra : IsRightRegular.{u_1} (R := R) 0
⊢ False
have rcases : ∀ (x y : R) (xy : x ≠ y), False
Tactic: rcases exists_pair_ne R with ⟨x, y, xy⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
ra : IsRightRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
⊢ False
have refine : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * 0) x) ((fun (x : R) ↦ x * 0) y)
Tactic: refine xy (ra ?_)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsLeftRegular b
| b * a = 0
have rw : b * a = b * 0
Tactic: rw [← mul_zero b]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = 0 ↔ a = 0
have conv_lhs : b * a = b * 0 ↔ a = 0
Tactic: conv_lhs => rw [← mul_zero b]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * a = b * 0
have rw : b * 0 = b * 0
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsRightRegular b
| a * b = 0
have rw : a * b = 0 * b
Tactic: rw [← zero_mul b]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 ↔ a = 0
have conv_lhs : a * b = 0 * b ↔ a = 0
Tactic: conv_lhs => rw [← zero_mul b]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Regular (goal)
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ a * b = 0 * b
have rw : 0 * b = 0 * b
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹
have pos : ∀ (ha : a = 0), SemiconjBy a x⁻¹ y⁻¹
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
pos : ∀ (ha : a = 0), SemiconjBy a x⁻¹ y⁻¹
⊢ SemiconjBy a x⁻¹ y⁻¹
have neg : ∀ (ha : ¬a = 0), SemiconjBy a x⁻¹ y⁻¹
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
have pos : ∀ (hx : x = 0), SemiconjBy a x⁻¹ y⁻¹
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
pos : ∀ (hx : x = 0), SemiconjBy a x⁻¹ y⁻¹
⊢ SemiconjBy a x⁻¹ y⁻¹
have neg : ∀ (hx : ¬x = 0), SemiconjBy a x⁻¹ y⁻¹
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
have pos : ∀ (h : SemiconjBy a 0 y), SemiconjBy a 0⁻¹ y⁻¹
Tactic: subst x
Cleared hypotheses: x, h, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (hypothesis)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹
have h₁ : y = 0 ∨ a = 0
Tactic: simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (hypothesis)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
have this : a * x ≠ 0
Tactic: have := mul_ne_zero ha hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (hypothesis)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
have this₁ : y ≠ 0 ∧ a ≠ 0
Tactic: rw [h.eq, mul_ne_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Semiconj (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x / x') (y / y')
have rw : SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Submonoid.Instances (goal)
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
⊢ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) (↑x : H)⁻¹
have obtain : ∀ (y : G) (hy : (f : (a : G) → H) y = (↑x : H)), Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) (↑x : H)⁻¹
Tactic: obtain ⟨y, hy⟩ := x.prop
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Submonoid.Instances (goal)
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
y : G
hy : (f : (a : G) → H) y = (↑x : H)
⊢ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) (↑x : H)⁻¹
have h : (f : (a : G) → H) y⁻¹ = (↑x : H)⁻¹
Tactic: use y⁻¹
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Submonoid.Instances (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
a : H
ha : Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) a
h : Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) a ha ≠ 0
⊢ Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) a ha *
      Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x)
        (↑(Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) a ha) : H)⁻¹ ⋯ =
    1
have h₁ : ¬a = (↑0 : H)
Tactic: simp only [ne_eq, Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Submonoid.Instances (goal)
Goal:
H : Type u_2
inst : CommGroupWithZero H
⊢ Eq (α := Submonoid H) (MonoidHom.mker (F := H →*₀ H) MonoidWithZero.inverse) ⊥
have h : ∀ (x : H),
  Membership.mem (γ := Submonoid H) (MonoidHom.mker (F := H →*₀ H) MonoidWithZero.inverse) x ↔
    Membership.mem (γ := Submonoid H) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
⊢ IsMulTorsionFree M
have refine : ∀ (n : ℕ) (hn : n ≠ 0) (x y : M) (hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)),
  x = y
Tactic: refine ⟨fun n hn x y hxy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
⊢ x = y
have pos : ∀ (h : x ≠ 0 ∧ y ≠ 0), x = y
Tactic: by_cases h : x ≠ 0 ∧ y ≠ 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
pos : ∀ (h : x ≠ 0 ∧ y ≠ 0), x = y
⊢ x = y
have neg : ∀ (h : ¬(x ≠ 0 ∧ y ≠ 0)), x = y
Tactic: by_cases h : x ≠ 0 ∧ y ≠ 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
h : ¬(x ≠ 0 ∧ y ≠ 0)
⊢ x = y
have this : IsReduced M
Tactic: have : IsReduced M := inferInstance
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
⊢ IsMulTorsionFree M
have refine : ∀ (x : M) (hx : x ≠ 0) (y : M) (hy : y ≠ 0) (n : ℕ) (hn : n ≠ 0) (hxy : x ^ n = y ^ n), x = y
Tactic: refine .mk' fun x hx y hy n hn hxy ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
⊢ Associated x y
have this : normalizedFactors (x ^ n) = normalizedFactors (y ^ n)
Tactic: have := (Associated.of_eq hxy).normalizedFactors_eq
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors (x ^ n) = normalizedFactors (y ^ n)
⊢ Associated x y
have rwa : ∀ (this : n • normalizedFactors x = normalizedFactors (y ^ n)), Associated x y
Tactic: rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors (x ^ n) = normalizedFactors (y ^ n)
rwa : ∀ (this : n • normalizedFactors x = normalizedFactors (y ^ n)), Associated x y
⊢ Associated x y
have rwa₁ : ∀ (this : n • normalizedFactors x = n • normalizedFactors y), Associated x y
Tactic: rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors (x ^ n) = normalizedFactors (y ^ n)
rwa : ∀ (this : n • normalizedFactors x = normalizedFactors (y ^ n)), Associated x y
rwa₁ : ∀ (this : n • normalizedFactors x = n • normalizedFactors y), Associated x y
⊢ Associated x y
have rwa₂ : ∀ (this : normalizedFactors x = normalizedFactors y), Associated x y
Tactic: rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors (x ^ n) = normalizedFactors (y ^ n)
rwa : ∀ (this : n • normalizedFactors x = normalizedFactors (y ^ n)), Associated x y
rwa₁ : ∀ (this : n • normalizedFactors x = n • normalizedFactors y), Associated x y
rwa₂ : ∀ (this : normalizedFactors x = normalizedFactors y), Associated x y
⊢ Associated x y
have rwa₃ : ∀ (this : Associated x y), Associated x y
Tactic: rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
⊢ x = y
have obtain : ∀ (u : Mˣ) (hu : x * (↑u : M) = y), x = y
Tactic: obtain ⟨u, hu⟩ : Associated x y := by
    have := (Associated.of_eq hxy).normalizedFactors_eq
    rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * (↑u : M) = y
⊢ x = y
have hx₁ : IsLeftRegular (x ^ n)
Tactic: replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
have hxy₁ : u = 1
Tactic: rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
    Units.val_eq_one, pow_eq_one_iff_left hn] at hxy
Cleared hypotheses: hxy, hu, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
have rwa : ∀ (hu : x * (↑1 : M) = y) (hx : IsLeftRegular (x ^ n)), x = y
Tactic: rwa [hxy, Units.val_one, mul_one] at hu
Cleared hypotheses: hu, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
rwa : ∀ (hu : x * (↑1 : M) = y) (hx : IsLeftRegular (x ^ n)), x = y
⊢ x = y
have rwa₁ : ∀ (hu : x * 1 = y) (hx : IsLeftRegular (x ^ n)), x = y
Tactic: rwa [hxy, Units.val_one, mul_one] at hu
Cleared hypotheses: hu, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Torsion (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
rwa : ∀ (hu : x * (↑1 : M) = y) (hx : IsLeftRegular (x ^ n)), x = y
rwa₁ : ∀ (hu : x * 1 = y) (hx : IsLeftRegular (x ^ n)), x = y
⊢ x = y
have rwa₂ : ∀ (hu : x = y) (hx : IsLeftRegular (x ^ n)), x = y
Tactic: rwa [hxy, Units.val_one, mul_one] at hu
Cleared hypotheses: hu, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
⊢ SemigroupWithZero α
have zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.semigroupWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
⊢ SemigroupWithZero α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.semigroupWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
⊢ MulZeroClass α
have zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.mulZeroClass _