awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
have rw : ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Tactic: rw [not_iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
⊢ b * a = 1
have rw : b * a * b = 1 * b
Tactic: rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : b * a * b = 1 * b
⊢ b * a = 1
have rw₁ : b * (a * b) = 1 * b
Tactic: rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : b * a * b = 1 * b
rw₁ : b * (a * b) = 1 * b
⊢ b * a = 1
have rw₂ : b * 1 = 1 * b
Tactic: rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : b * a * b = 1 * b
rw₁ : b * (a * b) = 1 * b
rw₂ : b * 1 = 1 * b
⊢ b * a = 1
have rw₃ : b * 1 = b
Tactic: rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : b * a * b = 1 * b
rw₁ : b * (a * b) = 1 * b
rw₂ : b * 1 = 1 * b
rw₃ : b * 1 = b
⊢ b * a = 1
have rw₄ : b = b
Tactic: rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
⊢ b = 1
have rwa : ∀ (h : 1 * b = 1), b = 1
Tactic: rwa [RightCancelMonoid.eq_one_of_mul_right h, one_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rwa : ∀ (h : 1 * b = 1), b = 1
⊢ b = 1
have rwa₁ : ∀ (h : b = 1), b = 1
Tactic: rwa [RightCancelMonoid.eq_one_of_mul_right h, one_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
have rw : ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Tactic: rw [not_iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
u : αˣ
⊢ x /ₚ u * y = x * y /ₚ u
have rw : x * (↑u⁻¹ : α) * y = x * y /ₚ u
Tactic: rw [divp, divp, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
u : αˣ
rw : x * (↑u⁻¹ : α) * y = x * y /ₚ u
⊢ x /ₚ u * y = x * y /ₚ u
have rw₁ : x * (↑u⁻¹ : α) * y = x * y * (↑u⁻¹ : α)
Tactic: rw [divp, divp, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
u : αˣ
rw : x * (↑u⁻¹ : α) * y = x * y /ₚ u
rw₁ : x * (↑u⁻¹ : α) * y = x * y * (↑u⁻¹ : α)
⊢ x /ₚ u * y = x * y /ₚ u
have rw₂ : x * y * (↑u⁻¹ : α) = x * y * (↑u⁻¹ : α)
Tactic: rw [divp, divp, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux = y /ₚ uy ↔ x * (↑uy : α) = y * (↑ux : α)
have rw : y /ₚ uy * (↑ux : α) = x ↔ x * (↑uy : α) = y * (↑ux : α)
Tactic: rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
rw : y /ₚ uy * (↑ux : α) = x ↔ x * (↑uy : α) = y * (↑ux : α)
⊢ x /ₚ ux = y /ₚ uy ↔ x * (↑uy : α) = y * (↑ux : α)
have rw₁ : y * (↑ux : α) /ₚ uy = x ↔ x * (↑uy : α) = y * (↑ux : α)
Tactic: rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
rw : y /ₚ uy * (↑ux : α) = x ↔ x * (↑uy : α) = y * (↑ux : α)
rw₁ : y * (↑ux : α) /ₚ uy = x ↔ x * (↑uy : α) = y * (↑ux : α)
⊢ x /ₚ ux = y /ₚ uy ↔ x * (↑uy : α) = y * (↑ux : α)
have rw₂ : x * (↑uy : α) = y * (↑ux : α) ↔ x * (↑uy : α) = y * (↑ux : α)
Tactic: rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
have rw : x * (y /ₚ uy) /ₚ ux = x * y /ₚ (ux * uy)
Tactic: rw [divp_mul_eq_mul_divp, ← divp_assoc, divp_divp_eq_divp_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
rw : x * (y /ₚ uy) /ₚ ux = x * y /ₚ (ux * uy)
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
have rw₁ : x * y /ₚ uy /ₚ ux = x * y /ₚ (ux * uy)
Tactic: rw [divp_mul_eq_mul_divp, ← divp_assoc, divp_divp_eq_divp_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
rw : x * (y /ₚ uy) /ₚ ux = x * y /ₚ (ux * uy)
rw₁ : x * y /ₚ uy /ₚ ux = x * y /ₚ (ux * uy)
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
have rw₂ : x * y /ₚ (ux * uy) = x * y /ₚ (ux * uy)
Tactic: rw [divp_mul_eq_mul_divp, ← divp_assoc, divp_divp_eq_divp_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
have rw : ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Tactic: rw [not_iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit b
⊢ 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.Group.Units.Basic (goal)
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit b
⊢ a * b = 1 * b ↔ a = 1
have rw : a = 1 ↔ a = 1
Tactic: rw [h.mul_left_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit a
⊢ 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.Group.Units.Basic (goal)
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit a
⊢ a * b = a * 1 ↔ b = 1
have rw : b = 1 ↔ b = 1
Tactic: rw [h.mul_right_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a / b * b = a
have rw : a * b⁻¹ * b = a
Tactic: rw [div_eq_mul_inv, h.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
rw : a * b⁻¹ * b = a
⊢ a / b * b = a
have rw₁ : a = a
Tactic: rw [div_eq_mul_inv, h.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b / b = a
have rw : a * b * b⁻¹ = a
Tactic: rw [div_eq_mul_inv, h.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
rw : a * b * b⁻¹ = a
⊢ a * b / b = a
have rw₁ : a = a
Tactic: rw [div_eq_mul_inv, h.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b
have simp : a * c⁻¹ = b * c⁻¹ ↔ a = b
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b
have rw : a * b⁻¹ = c ↔ a = c * b
Tactic: rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit b
rw : a * b⁻¹ = c ↔ a = c * b
⊢ a / b = c ↔ a = c * b
have rw₁ : a = c * b ↔ a = c * b
Tactic: rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b
have rw : a = b * c⁻¹ ↔ a * c = b
Tactic: rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
rw : a = b * c⁻¹ ↔ a * c = b
⊢ a = b / c ↔ a * c = b
have rw₁ : a * c = b ↔ a * c = b
Tactic: rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit b
⊢ b / (a * b) = 1 / a
have rw : a⁻¹ = 1 / a
Tactic: rw [h.div_mul_cancel_right, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit b
rw : a⁻¹ = 1 / a
⊢ b / (a * b) = 1 / a
have rw₁ : a⁻¹ = a⁻¹
Tactic: rw [h.div_mul_cancel_right, one_div]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b
have rw : a / (b * a) = 1 / b
Tactic: rw [mul_comm, h.div_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : a / (b * a) = 1 / b
⊢ a / (a * b) = 1 / b
have rw₁ : 1 / b = 1 / b
Tactic: rw [mul_comm, h.div_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * b / a = b
have rw : b * a / a = b
Tactic: rw [mul_comm, h.mul_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : b * a / a = b
⊢ a * b / a = b
have rw₁ : b = b
Tactic: rw [mul_comm, h.mul_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * (b / a) = b
have rw : b / a * a = b
Tactic: rw [mul_comm, h.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : b / a * a = b
⊢ a * (b / a) = b
have rw₁ : b = b
Tactic: rw [mul_comm, h.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * d = c * b
have rw : a * 1 * d = c * b
Tactic: rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
rw : a * 1 * d = c * b
⊢ a * d = c * b
have rw₁ : a * (b / b) * d = c * b
Tactic: rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
⊢ a * d = c * b
have rw₂ : a / b * b * d = c * b
Tactic: rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
rw₂ : a / b * b * d = c * b
⊢ a * d = c * b
have rw₃ : c / d * b * d = c * b
Tactic: rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
rw₂ : a / b * b * d = c * b
rw₃ : c / d * b * d = c * b
⊢ a * d = c * b
have rw₄ : c * b / d * d = c * b
Tactic: rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
rw₂ : a / b * b * d = c * b
rw₃ : c / d * b * d = c * b
rw₄ : c * b / d * d = c * b
⊢ a * d = c * b
have rw₅ : c * b = c * b
Tactic: rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b
have rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
Tactic: rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
⊢ a / b = c / d ↔ a * d = c * b
have rw₁ : a / b * b * d = c / d * (b * d) ↔ a * d = c * b
Tactic: rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
rw₁ : a / b * b * d = c / d * (b * d) ↔ a * d = c * b
⊢ a / b = c / d ↔ a * d = c * b
have rw₂ : a * d = c / d * (b * d) ↔ a * d = c * b
Tactic: rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
rw₁ : a / b * b * d = c / d * (b * d) ↔ a * d = c * b
rw₂ : a * d = c / d * (b * d) ↔ a * d = c * b
⊢ a / b = c / d ↔ a * d = c * b
have rw₃ : a * d = c / d * b * d ↔ a * d = c * b
Tactic: rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
rw₁ : a / b * b * d = c / d * (b * d) ↔ a * d = c * b
rw₂ : a * d = c / d * (b * d) ↔ a * d = c * b
rw₃ : a * d = c / d * b * d ↔ a * d = c * b
⊢ a / b = c / d ↔ a * d = c * b
have rw₄ : a * d = c / d * d * b ↔ a * d = c * b
Tactic: rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
rw₁ : a / b * b * d = c / d * (b * d) ↔ a * d = c * b
rw₂ : a * d = c / d * (b * d) ↔ a * d = c * b
rw₃ : a * d = c / d * b * d ↔ a * d = c * b
rw₄ : a * d = c / d * d * b ↔ a * d = c * b
⊢ a / b = c / d ↔ a * d = c * b
have rw₅ : a * d = c * b ↔ a * d = c * b
Tactic: rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b
have rw : a / b = c * d⁻¹ ↔ a * d = c * b
Tactic: rw [← div_eq_mul_inv, ← div_eq_mul_inv, hb.div_eq_div_iff hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b = c * d⁻¹ ↔ a * d = c * b
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b
have rw₁ : a / b = c / d ↔ a * d = c * b
Tactic: rw [← div_eq_mul_inv, ← div_eq_mul_inv, hb.div_eq_div_iff hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b = c * d⁻¹ ↔ a * d = c * b
rw₁ : a / b = c / d ↔ a * d = c * b
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b
have rw₂ : a * d = c * b ↔ a * d = c * b
Tactic: rw [← div_eq_mul_inv, ← div_eq_mul_inv, hb.div_eq_div_iff hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b
have rw : a / b = d⁻¹ * c ↔ a * d = c * b
Tactic: rw [← div_eq_inv_mul, ← div_eq_inv_mul, hb.div_eq_div_iff hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b = d⁻¹ * c ↔ a * d = c * b
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b
have rw₁ : a / b = c / d ↔ a * d = c * b
Tactic: rw [← div_eq_inv_mul, ← div_eq_inv_mul, hb.div_eq_div_iff hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b = d⁻¹ * c ↔ a * d = c * b
rw₁ : a / b = c / d ↔ a * d = c * b
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b
have rw₂ : a * d = c * b ↔ a * d = c * b
Tactic: rw [← div_eq_inv_mul, ← div_eq_inv_mul, hb.div_eq_div_iff hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / (a / b) = b
have rw : a * b / a = b
Tactic: rw [div_div_eq_mul_div, h.mul_div_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
rw : a * b / a = b
⊢ a / (a / b) = b
have rw₁ : b = b
Tactic: rw [div_div_eq_mul_div, h.mul_div_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / b / a = b⁻¹
have rw : a / b * a⁻¹ = b⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
rw : a / b * a⁻¹ = b⁻¹
⊢ a / b / a = b⁻¹
have rw₁ : a * b⁻¹ * a⁻¹ = b⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
rw : a / b * a⁻¹ = b⁻¹
rw₁ : a * b⁻¹ * a⁻¹ = b⁻¹
⊢ a / b / a = b⁻¹
have rw₂ : a * a⁻¹ * b⁻¹ = b⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
rw : a / b * a⁻¹ = b⁻¹
rw₁ : a * b⁻¹ * a⁻¹ = b⁻¹
rw₂ : a * a⁻¹ * b⁻¹ = b⁻¹
⊢ a / b / a = b⁻¹
have rw₃ : 1 * b⁻¹ = b⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
rw : a / b * a⁻¹ = b⁻¹
rw₁ : a * b⁻¹ * a⁻¹ = b⁻¹
rw₂ : a * a⁻¹ * b⁻¹ = b⁻¹
rw₃ : 1 * b⁻¹ = b⁻¹
⊢ a / b / a = b⁻¹
have rw₄ : b⁻¹ = b⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ : αˣ } =
    { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
have subst : ∀ (vi₂ : v * i₂ = 1) (iv₂ : i₂ * v = 1),
  { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ : αˣ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }
Tactic: subst v'
Cleared hypotheses: v', vi₂, iv₂, e
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ : αˣ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }
have e_inv : i₁ = i₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
⊢ (↑u₁ : α) * (↑u₂ : α) * (u₂.inv * u₁.inv) = 1
have rw : (↑u₁ : α) * ((↑u₂ : α) * (u₂.inv * u₁.inv)) = 1
Tactic: rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑u₁ : α) * ((↑u₂ : α) * (u₂.inv * u₁.inv)) = 1
⊢ (↑u₁ : α) * (↑u₂ : α) * (u₂.inv * u₁.inv) = 1
have rw₁ : (↑u₁ : α) * ((↑u₂ : α) * u₂.inv * u₁.inv) = 1
Tactic: rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑u₁ : α) * ((↑u₂ : α) * (u₂.inv * u₁.inv)) = 1
rw₁ : (↑u₁ : α) * ((↑u₂ : α) * u₂.inv * u₁.inv) = 1
⊢ (↑u₁ : α) * (↑u₂ : α) * (u₂.inv * u₁.inv) = 1
have rw₂ : (↑u₁ : α) * (1 * u₁.inv) = 1
Tactic: rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑u₁ : α) * ((↑u₂ : α) * (u₂.inv * u₁.inv)) = 1
rw₁ : (↑u₁ : α) * ((↑u₂ : α) * u₂.inv * u₁.inv) = 1
rw₂ : (↑u₁ : α) * (1 * u₁.inv) = 1
⊢ (↑u₁ : α) * (↑u₂ : α) * (u₂.inv * u₁.inv) = 1
have rw₃ : (↑u₁ : α) * u₁.inv = 1
Tactic: rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑u₁ : α) * ((↑u₂ : α) * (u₂.inv * u₁.inv)) = 1
rw₁ : (↑u₁ : α) * ((↑u₂ : α) * u₂.inv * u₁.inv) = 1
rw₂ : (↑u₁ : α) * (1 * u₁.inv) = 1
rw₃ : (↑u₁ : α) * u₁.inv = 1
⊢ (↑u₁ : α) * (↑u₂ : α) * (u₂.inv * u₁.inv) = 1
have rw₄ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * u₁.inv * ((↑u₁ : α) * (↑u₂ : α)) = 1
have rw : u₂.inv * (u₁.inv * ((↑u₁ : α) * (↑u₂ : α))) = 1
Tactic: rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : u₂.inv * (u₁.inv * ((↑u₁ : α) * (↑u₂ : α))) = 1
⊢ u₂.inv * u₁.inv * ((↑u₁ : α) * (↑u₂ : α)) = 1
have rw₁ : u₂.inv * (u₁.inv * (↑u₁ : α) * (↑u₂ : α)) = 1
Tactic: rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : u₂.inv * (u₁.inv * ((↑u₁ : α) * (↑u₂ : α))) = 1
rw₁ : u₂.inv * (u₁.inv * (↑u₁ : α) * (↑u₂ : α)) = 1
⊢ u₂.inv * u₁.inv * ((↑u₁ : α) * (↑u₂ : α)) = 1
have rw₂ : u₂.inv * (1 * (↑u₂ : α)) = 1
Tactic: rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : u₂.inv * (u₁.inv * ((↑u₁ : α) * (↑u₂ : α))) = 1
rw₁ : u₂.inv * (u₁.inv * (↑u₁ : α) * (↑u₂ : α)) = 1
rw₂ : u₂.inv * (1 * (↑u₂ : α)) = 1
⊢ u₂.inv * u₁.inv * ((↑u₁ : α) * (↑u₂ : α)) = 1
have rw₃ : u₂.inv * (↑u₂ : α) = 1
Tactic: rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]