awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
rw₁ : 1 = 1 * HPow.hPow (β := ℕ) b 0
rw₂ : 1 = HMul.hMul (α := M) 1 1
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw₃ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
hab : Commute a b
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have rw : (b * a)⁻¹ = a⁻¹ * b⁻¹
Tactic: rw [hab.eq, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
hab : Commute a b
rw : (b * a)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have rw₁ : a⁻¹ * b⁻¹ = a⁻¹ * b⁻¹
Tactic: rw [hab.eq, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
⊢ a * b * a⁻¹ = b
have rw : b * a * a⁻¹ = b
Tactic: rw [h.eq, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : b * a * a⁻¹ = b
⊢ a * b * a⁻¹ = b
have rw₁ : b = b
Tactic: rw [h.eq, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
⊢ a * (b * a⁻¹) = b
have rw : a * b * a⁻¹ = b
Tactic: rw [← mul_assoc, h.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : a * b * a⁻¹ = b
⊢ a * (b * a⁻¹) = b
have rw₁ : b = b
Tactic: rw [← mul_assoc, h.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
⊢ a * (b * (↑u⁻¹ : M)) = 1
have rw : a * b * (↑u⁻¹ : M) = 1
Tactic: rw [← mul_assoc, hu, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
rw : a * b * (↑u⁻¹ : M) = 1
⊢ a * (b * (↑u⁻¹ : M)) = 1
have rw₁ : (↑u : M) * (↑u⁻¹ : M) = 1
Tactic: rw [← mul_assoc, hu, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
rw : a * b * (↑u⁻¹ : M) = 1
rw₁ : (↑u : M) * (↑u⁻¹ : M) = 1
⊢ a * (b * (↑u⁻¹ : M)) = 1
have rw₂ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← mul_assoc, hu, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (hypothesis)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
⊢ b * (↑u⁻¹ : M) * a = 1
have this : Commute a (↑u : M)
Tactic: have : Commute a u := hu ▸ (Commute.refl _).mul_right hc
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
this : Commute a (↑u : M)
⊢ b * (↑u⁻¹ : M) * a = 1
have rw : b * a * (↑u⁻¹ : M) = 1
Tactic: rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
this : Commute a (↑u : M)
rw : b * a * (↑u⁻¹ : M) = 1
⊢ b * (↑u⁻¹ : M) * a = 1
have rw₁ : a * b * (↑u⁻¹ : M) = 1
Tactic: rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
this : Commute a (↑u : M)
rw : b * a * (↑u⁻¹ : M) = 1
rw₁ : a * b * (↑u⁻¹ : M) = 1
⊢ b * (↑u⁻¹ : M) * a = 1
have rw₂ : (↑u : M) * (↑u⁻¹ : M) = 1
Tactic: rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
this : Commute a (↑u : M)
rw : b * a * (↑u⁻¹ : M) = 1
rw₁ : a * b * (↑u⁻¹ : M) = 1
rw₂ : (↑u : M) * (↑u⁻¹ : M) = 1
⊢ b * (↑u⁻¹ : M) * a = 1
have rw₃ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
n_1 : ℕ
a b : M
u_1 u₁ u₂ u : Mˣ
x : M
n : ℕ
hn : n ≠ 0
hu : x ^ n = (↑u : M)
⊢ x * x ^ (n - 1) = (↑u : M)
have rwa : x ^ (n - 1 + 1) = (↑u : M)
Tactic: rwa [← _root_.pow_succ', Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ n) ↔ n = 0
have zero : IsUnit (HPow.hPow (β := ℕ) a 0) ↔ Eq (α := ℕ) 0 0
Tactic: rcases n with (_ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
zero : IsUnit (HPow.hPow (β := ℕ) a 0) ↔ Eq (α := ℕ) 0 0
⊢ IsUnit (a ^ n) ↔ n = 0
have succ : ∀ (n : ℕ), IsUnit (a ^ (n + 1)) ↔ n + 1 = 0
Tactic: rcases n with (_ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * a * (↑u : M) = a
have rw : Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
Tactic: rw [mul_assoc, Units.inv_mul_eq_iff_eq_mul, eq_comm, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * a * (↑u : M) = a
have rw₁ : Commute (↑u : M) a ↔ a * (↑u : M) = (↑u : M) * a
Tactic: rw [mul_assoc, Units.inv_mul_eq_iff_eq_mul, eq_comm, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
rw₁ : Commute (↑u : M) a ↔ a * (↑u : M) = (↑u : M) * a
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * a * (↑u : M) = a
have rw₂ : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
Tactic: rw [mul_assoc, Units.inv_mul_eq_iff_eq_mul, eq_comm, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
rw₁ : Commute (↑u : M) a ↔ a * (↑u : M) = (↑u : M) * a
rw₂ : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * a * (↑u : M) = a
have rw₃ : SemiconjBy (↑u : M) a a ↔ (↑u : M) * a = a * (↑u : M)
Tactic: rw [mul_assoc, Units.inv_mul_eq_iff_eq_mul, eq_comm, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
rw₁ : Commute (↑u : M) a ↔ a * (↑u : M) = (↑u : M) * a
rw₂ : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
rw₃ : SemiconjBy (↑u : M) a a ↔ (↑u : M) * a = a * (↑u : M)
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * a * (↑u : M) = a
have rw₄ : (↑u : M) * a = a * (↑u : M) ↔ (↑u : M) * a = a * (↑u : M)
Tactic: rw [mul_assoc, Units.inv_mul_eq_iff_eq_mul, eq_comm, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
have rw : (↑u⁻¹ : M) * a * (↑u : M) = a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
Tactic: rw [u.commute_iff_inv_mul_cancel, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : (↑u⁻¹ : M) * a * (↑u : M) = a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
have rw₁ : (↑u⁻¹ : M) * (a * (↑u : M)) = a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
Tactic: rw [u.commute_iff_inv_mul_cancel, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u : M) a ↔ (↑u : M) * a * (↑u⁻¹ : M) = a
have rw : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
Tactic: rw [Units.mul_inv_eq_iff_eq_mul, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
⊢ Commute (↑u : M) a ↔ (↑u : M) * a * (↑u⁻¹ : M) = a
have rw₁ : SemiconjBy (↑u : M) a a ↔ (↑u : M) * a = a * (↑u : M)
Tactic: rw [Units.mul_inv_eq_iff_eq_mul, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
rw₁ : SemiconjBy (↑u : M) a a ↔ (↑u : M) * a = a * (↑u : M)
⊢ Commute (↑u : M) a ↔ (↑u : M) * a * (↑u⁻¹ : M) = a
have rw₂ : (↑u : M) * a = a * (↑u : M) ↔ (↑u : M) * a = a * (↑u : M)
Tactic: rw [Units.mul_inv_eq_iff_eq_mul, Commute, SemiconjBy]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u : M) a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a
have rw : (↑u : M) * a * (↑u⁻¹ : M) = a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a
Tactic: rw [u.commute_iff_mul_inv_cancel, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : (↑u : M) * a * (↑u⁻¹ : M) = a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a
⊢ Commute (↑u : M) a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a
have rw₁ : (↑u : M) * (a * (↑u⁻¹ : M)) = a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a
Tactic: rw [u.commute_iff_mul_inv_cancel, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.right_comm,
    hd.div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.div_eq_div_iff_of_isUnit hb hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.div_eq_div_iff_of_isUnit hb hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b 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, hbd.div_eq_div_iff_of_isUnit hb hd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₄ : d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₄ : d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₅ : d * a = d * b * d⁻¹ * c ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₄ : d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₅ : d * a = d * b * d⁻¹ * c ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₆ : d * a = d * (b * d⁻¹) * c ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₄ : d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₅ : d * a = d * b * d⁻¹ * c ↔ d * a = b * c
rw₆ : d * a = d * (b * d⁻¹) * c ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₇ : d * a = b * (d * d⁻¹) * c ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₄ : d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₅ : d * a = d * b * d⁻¹ * c ↔ d * a = b * c
rw₆ : d * a = d * (b * d⁻¹) * c ↔ d * a = b * c
rw₇ : d * a = b * (d * d⁻¹) * c ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₈ : d * a = b * 1 * c ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Units (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₄ : d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₅ : d * a = d * b * d⁻¹ * c ↔ d * a = b * c
rw₆ : d * a = d * (b * d⁻¹) * c ↔ d * a = b * c
rw₇ : d * a = b * (d * d⁻¹) * c ↔ d * a = b * c
rw₈ : d * a = b * 1 * c ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c
have rw₉ : d * a = b * c ↔ d * a = b * c
Tactic: rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b
have rw : IsConj b b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c : α) a b
⊢ SemiconjBy.{v} (M := β) ((↑((Units.map f : (a : αˣ) → βˣ) c) : β) : β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)
have rw : SemiconjBy.{v} (M := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
Tactic: rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c : α) a b
rw : SemiconjBy.{v} (M := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
⊢ SemiconjBy.{v} (M := β) ((↑((Units.map f : (a : αˣ) → βˣ) c) : β) : β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)
have rw₁ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) =
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
Tactic: rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c : α) a b
rw : SemiconjBy.{v} (M := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
rw₁ :
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
⊢ SemiconjBy.{v} (M := β) ((↑((Units.map f : (a : αˣ) → βˣ) c) : β) : β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)
have rw₂ : (f : (a : α) → β) ((↑c : α) * a) =
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
Tactic: rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c : α) a b
rw : SemiconjBy.{v} (M := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
rw₁ :
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
rw₂ :
  (f : (a : α) → β) ((↑c : α) * a) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
⊢ SemiconjBy.{v} (M := β) ((↑((Units.map f : (a : αˣ) → βˣ) c) : β) : β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)
have rw₃ : (f : (a : α) → β) (b * (↑c : α)) =
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
Tactic: rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]