awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
rw : n /. x * (d /. x)⁻¹ = n /. d
rw₁ : n /. x * (x /. d) = n /. d
⊢ n /. x / (d /. x) = n /. d
have rw₂ : n /. d = n /. d
Tactic: rw [div_eq_mul_inv, inv_divInt, divInt_mul_divInt_cancel hx]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n / (x /. d) = d /. n
have rw : x /. n * (x /. d)⁻¹ = d /. n
Tactic: rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
rw : x /. n * (x /. d)⁻¹ = d /. n
⊢ x /. n / (x /. d) = d /. n
have rw₁ : x /. n * (d /. x) = d /. n
Tactic: rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
rw : x /. n * (x /. d)⁻¹ = d /. n
rw₁ : x /. n * (d /. x) = d /. n
⊢ x /. n / (x /. d) = d /. n
have rw₂ : d /. x * (x /. n) = d /. n
Tactic: rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
rw : x /. n * (x /. d)⁻¹ = d /. n
rw₁ : x /. n * (d /. x) = d /. n
rw₂ : d /. x * (x /. n) = d /. n
⊢ x /. n / (x /. d) = d /. n
have rw₃ : d /. n = d /. n
Tactic: rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
r : ℚ
⊢ HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ) = r
have rw : HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑(↑r.den : ℤ) : ℚ) = r
Tactic: rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
r : ℚ
rw : HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑(↑r.den : ℤ) : ℚ) = r
⊢ HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ) = r
have rw₁ : r.num /. (↑r.den : ℤ) = r
Tactic: rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
r : ℚ
rw : HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑(↑r.den : ℤ) : ℚ) = r
rw₁ : r.num /. (↑r.den : ℤ) = r
⊢ HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ) = r
have rw₂ : r = r
Tactic: rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
num den n : ℕ
⊢ mkRat (↑num : ℤ) den ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
have rw : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
Tactic: rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
num den n : ℕ
rw : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
⊢ mkRat (↑num : ℤ) den ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
have rw₁ : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = HPow.hPow (α := ℤ) (↑num : ℤ) n /. (↑(den ^ n) : ℤ)
Tactic: rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
num den n : ℕ
rw : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
rw₁ : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = HPow.hPow (α := ℤ) (↑num : ℤ) n /. (↑(den ^ n) : ℤ)
⊢ mkRat (↑num : ℤ) den ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
have rw₂ : HPow.hPow (α := ℤ) (↑num : ℤ) n /. HPow.hPow (α := ℤ) (↑den : ℤ) n = HPow.hPow (α := ℤ) (↑num : ℤ) n /. (↑(den ^ n) : ℤ)
Tactic: rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
num den n : ℕ
rw : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
rw₁ : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = HPow.hPow (α := ℤ) (↑num : ℤ) n /. (↑(den ^ n) : ℤ)
rw₂ :
  HPow.hPow (α := ℤ) (↑num : ℤ) n /. HPow.hPow (α := ℤ) (↑den : ℤ) n =
    HPow.hPow (α := ℤ) (↑num : ℤ) n /. (↑(den ^ n) : ℤ)
⊢ mkRat (↑num : ℤ) den ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
have rw₃ : HPow.hPow (α := ℤ) (↑num : ℤ) n /. HPow.hPow (α := ℤ) (↑den : ℤ) n =
  HPow.hPow (α := ℤ) (↑num : ℤ) n /. HPow.hPow (α := ℤ) (↑den : ℤ) n
Tactic: rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
n : ℕ
⊢ (↑n : ℚ) = (↑n : ℤ) /. 1
have rw : (↑(↑n : ℤ) : ℚ) = (↑n : ℤ) /. 1
Tactic: rw [← Int.cast_natCast, intCast_eq_divInt]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
n : ℕ
rw : (↑(↑n : ℤ) : ℚ) = (↑n : ℤ) /. 1
⊢ (↑n : ℚ) = (↑n : ℤ) /. 1
have rw₁ : (↑n : ℤ) /. 1 = (↑n : ℤ) /. 1
Tactic: rw [← Int.cast_natCast, intCast_eq_divInt]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
q : ℚ
⊢ q * (↑q.den : ℚ) = (↑q.num : ℚ)
have suffices : q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1
Tactic: suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by simp_all
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (hypothesis)
Goal:
q : ℚ
⊢ q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1
have this : Ne (α := ℤ) (↑q.den : ℤ) 0
Tactic: have : (q.den : ℤ) ≠ 0 := mod_cast q.den_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
q : ℚ
this : Ne (α := ℤ) (↑q.den : ℤ) 0
⊢ q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1
have rw : q.num * (↑q.den : ℤ) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) 1 = q.num /. 1
Tactic: rw [divInt_mul_divInt, mul_comm (q.den : ℤ) 1, divInt_mul_right this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
q : ℚ
this : Ne (α := ℤ) (↑q.den : ℤ) 0
rw : q.num * (↑q.den : ℤ) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) 1 = q.num /. 1
⊢ q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1
have rw₁ : q.num * (↑q.den : ℤ) /. HMul.hMul (α := ℤ) 1 (↑q.den : ℤ) = q.num /. 1
Tactic: rw [divInt_mul_divInt, mul_comm (q.den : ℤ) 1, divInt_mul_right this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
q : ℚ
this : Ne (α := ℤ) (↑q.den : ℤ) 0
rw : q.num * (↑q.den : ℤ) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) 1 = q.num /. 1
rw₁ : q.num * (↑q.den : ℤ) /. HMul.hMul (α := ℤ) 1 (↑q.den : ℤ) = q.num /. 1
⊢ q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1
have rw₂ : q.num /. 1 = q.num /. 1
Tactic: rw [divInt_mul_divInt, mul_comm (q.den : ℤ) 1, divInt_mul_right this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
q : ℚ
⊢ (↑q.den : ℚ) * q = (↑q.num : ℚ)
have rw : q * (↑q.den : ℚ) = (↑q.num : ℚ)
Tactic: rw [mul_comm, mul_den_eq_num]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Rat (goal)
Goal:
q : ℚ
rw : q * (↑q.den : ℚ) = (↑q.num : ℚ)
⊢ (↑q.den : ℚ) * q = (↑q.num : ℚ)
have rw₁ : Eq (α := ℚ) (↑q.num : ℚ) (↑q.num : ℚ)
Tactic: rw [mul_comm, mul_den_eq_num]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
⊢ IsLeftRegular k
have refine : ∀ (x y : α) (h' : k * x = k * y), k * (x - y) = 0
Tactic: refine fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * (x - y) = 0
have rw : k * x - k * y = 0
Tactic: rw [mul_sub, sub_eq_zero, h']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
rw : k * x - k * y = 0
rw₁ : k * x = k * y
⊢ k * (x - y) = 0
have rw₂ : k * y = k * y
Tactic: rw [mul_sub, sub_eq_zero, h']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
⊢ IsRightRegular k
have refine : ∀ (x y : α) (h' : x * k = y * k), (x - y) * k = 0
Tactic: refine fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ (x - y) * k = 0
have rw : x * k - y * k = 0
Tactic: rw [sub_mul, sub_eq_zero, h']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
rw : x * k - y * k = 0
rw₁ : x * k = y * k
⊢ (x - y) * k = 0
have rw₂ : y * k = y * k
Tactic: rw [sub_mul, sub_eq_zero, h']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
have refine_1 : ∀ (h : ∀ {a b : α}, a * b = 1 → b * a = 1) (x y z : α) (hxy : x * y = 1) (hxz : x * z = 1), y = z
Tactic: refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxy hxz ↦ ?_, fun h x y eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
refine_1 : ∀ (h : ∀ {a b : α}, a * b = 1 → b * a = 1) (x y z : α) (hxy : x * y = 1) (hxz : x * z = 1), y = z
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
have refine_2 : ∀ (h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z) (x y : α) (eq : x * y = 1), y * x = 1
Tactic: refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxy hxz ↦ ?_, fun h x y eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ x * (1 - y * x + y) = 1
have rw : x * (1 - y * x) + x * y = 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
⊢ x * (1 - y * x + y) = 1
have rw₁ : x * 1 - x * (y * x) + x * y = 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
rw₁ : x * 1 - x * (y * x) + x * y = 1
⊢ x * (1 - y * x + y) = 1
have rw₂ : x * 1 - x * y * x + x * y = 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
rw₁ : x * 1 - x * (y * x) + x * y = 1
rw₂ : x * 1 - x * y * x + x * y = 1
⊢ x * (1 - y * x + y) = 1
have rw₃ : x * 1 - 1 * x + 1 = 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
rw₁ : x * 1 - x * (y * x) + x * y = 1
rw₂ : x * 1 - x * y * x + x * y = 1
rw₃ : x * 1 - 1 * x + 1 = 1
⊢ x * (1 - y * x + y) = 1
have rw₄ : x - 1 * x + 1 = 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
rw₁ : x * 1 - x * (y * x) + x * y = 1
rw₂ : x * 1 - x * y * x + x * y = 1
rw₃ : x * 1 - 1 * x + 1 = 1
rw₄ : x - 1 * x + 1 = 1
⊢ x * (1 - y * x + y) = 1
have rw₅ : x - x + 1 = 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
rw₁ : x * 1 - x * (y * x) + x * y = 1
rw₂ : x * 1 - x * y * x + x * y = 1
rw₃ : x * 1 - 1 * x + 1 = 1
rw₄ : x - 1 * x + 1 = 1
rw₅ : x - x + 1 = 1
⊢ x * (1 - y * x + y) = 1
have rw₆ : HAdd.hAdd (α := α) 0 1 = 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
rw₁ : x * 1 - x * (y * x) + x * y = 1
rw₂ : x * 1 - x * y * x + x * y = 1
rw₃ : x * 1 - 1 * x + 1 = 1
rw₄ : x - 1 * x + 1 = 1
rw₅ : x - x + 1 = 1
rw₆ : HAdd.hAdd (α := α) 0 1 = 1
⊢ x * (1 - y * x + y) = 1
have rw₇ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (hypothesis)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ y * x = 1
have this : y = 1 - y * x + y
Tactic: have := h _ _ (1 - y * x + y) eq <| by
    rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y = 1 - y * x + y
⊢ y * x = 1
have refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
Tactic: rwa [right_eq_add, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y = 1 - y * x + y
refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
⊢ y * x = 1
have refine_2₁ : ∀ (this : 1 = y * x), y * x = 1
Tactic: rwa [right_eq_add, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y = 1 - y * x + y
refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
refine_2₁ : ∀ (this : 1 = y * x), y * x = 1
⊢ y * x = 1
have refine_2₂ : ∀ (this : y * x = 1), y * x = 1
Tactic: rwa [right_eq_add, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
have refine_1 : ∀ (h : ∀ {a b : α}, a * b = 1 → b * a = 1) (x y z : α) (hxz : x * z = 1) (hyz : y * z = 1), x = y
Tactic: refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxz hyz ↦ ?_, fun h x y eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
refine_1 : ∀ (h : ∀ {a b : α}, a * b = 1 → b * a = 1) (x y z : α) (hxz : x * z = 1) (hyz : y * z = 1), x = y
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
have refine_2 : ∀ (h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y) (x y : α) (eq : x * y = 1), y * x = 1
Tactic: refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxz hyz ↦ ?_, fun h x y eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ (1 - y * x + x) * y = 1
have rw : (1 - y * x) * y + x * y = 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
⊢ (1 - y * x + x) * y = 1
have rw₁ : 1 * y - y * x * y + x * y = 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
rw₁ : 1 * y - y * x * y + x * y = 1
⊢ (1 - y * x + x) * y = 1
have rw₂ : 1 * y - y * (x * y) + x * y = 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
rw₁ : 1 * y - y * x * y + x * y = 1
rw₂ : 1 * y - y * (x * y) + x * y = 1
⊢ (1 - y * x + x) * y = 1
have rw₃ : 1 * y - y * 1 + 1 = 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
rw₁ : 1 * y - y * x * y + x * y = 1
rw₂ : 1 * y - y * (x * y) + x * y = 1
rw₃ : 1 * y - y * 1 + 1 = 1
⊢ (1 - y * x + x) * y = 1
have rw₄ : y - y * 1 + 1 = 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
rw₁ : 1 * y - y * x * y + x * y = 1
rw₂ : 1 * y - y * (x * y) + x * y = 1
rw₃ : 1 * y - y * 1 + 1 = 1
rw₄ : y - y * 1 + 1 = 1
⊢ (1 - y * x + x) * y = 1
have rw₅ : y - y + 1 = 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
rw₁ : 1 * y - y * x * y + x * y = 1
rw₂ : 1 * y - y * (x * y) + x * y = 1
rw₃ : 1 * y - y * 1 + 1 = 1
rw₄ : y - y * 1 + 1 = 1
rw₅ : y - y + 1 = 1
⊢ (1 - y * x + x) * y = 1
have rw₆ : HAdd.hAdd (α := α) 0 1 = 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
rw₁ : 1 * y - y * x * y + x * y = 1
rw₂ : 1 * y - y * (x * y) + x * y = 1
rw₃ : 1 * y - y * 1 + 1 = 1
rw₄ : y - y * 1 + 1 = 1
rw₅ : y - y + 1 = 1
rw₆ : HAdd.hAdd (α := α) 0 1 = 1
⊢ (1 - y * x + x) * y = 1
have rw₇ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (hypothesis)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ y * x = 1
have this : x = 1 - y * x + x
Tactic: have := h _ (1 - y * x + x) _ eq <| by
    rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : x = 1 - y * x + x
⊢ y * x = 1
have refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
Tactic: rwa [right_eq_add, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : x = 1 - y * x + x
refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
⊢ y * x = 1
have refine_2₁ : ∀ (this : 1 = y * x), y * x = 1
Tactic: rwa [right_eq_add, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Regular (goal)
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : x = 1 - y * x + x
refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
refine_2₁ : ∀ (this : 1 = y * x), y * x = 1
⊢ y * x = 1
have refine_2₂ : ∀ (this : y * x = 1), y * x = 1
Tactic: rwa [right_eq_add, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Semireal.Defs (hypothesis)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : Eq.{u_1 + 1} (α := R) (↑(n + 1) : R) 0
⊢ n + 1 = 0
have hn₁ : Eq.{u_1 + 1} (α := R) (↑(1 + n) : R) 0
Tactic: rw [add_comm] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Semireal.Defs (hypothesis)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : Eq.{u_1 + 1} (α := R) (↑(1 + n) : R) 0
⊢ n + 1 = 0
have hn₁ : HAdd.hAdd (α := R) 1 (↑n : R) = 0
Tactic: push_cast at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Semireal.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : Eq.{u_1 + 1} (α := R) (↑n : R) 0
⊢ n = 0
have zero : ∀ (hn : Eq.{u_1 + 1} (α := R) (↑0 : R) 0), Eq (α := ℕ) 0 0
Tactic: cases n with
    | zero => rfl
    | succ n =>
      rw [add_comm] at hn
      push_cast at hn
      simpa using IsSemireal.one_add_ne_zero (by simp) hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Semireal.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : Eq.{u_1 + 1} (α := R) (↑n : R) 0
zero : ∀ (hn : Eq.{u_1 + 1} (α := R) (↑0 : R) 0), Eq (α := ℕ) 0 0
⊢ n = 0
have succ : ∀ (n : ℕ) (hn : Eq.{u_1 + 1} (α := R) (↑(n + 1) : R) 0), n + 1 = 0
Tactic: cases n with
    | zero => rfl
    | succ n =>
      rw [add_comm] at hn
      push_cast at hn
      simpa using IsSemireal.one_add_ne_zero (by simp) hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subgroup (goal)
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -(m * n) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
have rw : -m * n ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
Tactic: rw [← neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subgroup (goal)
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -(r₁ + r₂) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
have rw : -r₁ + -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
Tactic: rw [neg_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Basic (goal)
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : b ∈ S
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)
have mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b)
Tactic: induction ha using closure_induction with
  | mem r hr => exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)
  | zero => simp only [zero_mul, zero_mem _]
  | add r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Submonoid.Basic (goal)
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : b ∈ S
mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)
have zero : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (0 * b)
Tactic: induction ha using closure_induction with
  | mem r hr => exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)
  | zero => simp only [zero_mul, zero_mem _]
  | add r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs
Cleared hypotheses: ha