awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₃ : u₂.inv * (↑u₂ : α) = 1
⊢ u₂.inv * u₁.inv * ((↑u₁ : α) * (↑u₂ : α)) = 1
have rw₄ : Eq.{u + 1} (α := α) 1 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 α
a : αˣ
⊢ (↑a : α) = 1 ↔ a = 1
have rw : (↑a : α) = (↑1 : α) ↔ a = 1
Tactic: rw [← Units.val_one, val_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
rw : (↑a : α) = (↑1 : α) ↔ a = 1
⊢ (↑a : α) = 1 ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [← Units.val_one, val_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
⊢ Commute (↑a : α) (↑a⁻¹ : α)
have rw : SemiconjBy (↑a : α) (↑a⁻¹ : α) (↑a⁻¹ : α)
Tactic: rw [Commute, SemiconjBy, inv_mul, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
rw : SemiconjBy (↑a : α) (↑a⁻¹ : α) (↑a⁻¹ : α)
⊢ Commute (↑a : α) (↑a⁻¹ : α)
have rw₁ : (↑a : α) * (↑a⁻¹ : α) = (↑a⁻¹ : α) * (↑a : α)
Tactic: rw [Commute, SemiconjBy, inv_mul, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
rw : SemiconjBy (↑a : α) (↑a⁻¹ : α) (↑a⁻¹ : α)
rw₁ : (↑a : α) * (↑a⁻¹ : α) = (↑a⁻¹ : α) * (↑a : α)
⊢ Commute (↑a : α) (↑a⁻¹ : α)
have rw₂ : (↑a : α) * (↑a⁻¹ : α) = 1
Tactic: rw [Commute, SemiconjBy, inv_mul, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
rw : SemiconjBy (↑a : α) (↑a⁻¹ : α) (↑a⁻¹ : α)
rw₁ : (↑a : α) * (↑a⁻¹ : α) = (↑a⁻¹ : α) * (↑a : α)
rw₂ : (↑a : α) * (↑a⁻¹ : α) = 1
⊢ Commute (↑a : α) (↑a⁻¹ : α)
have rw₃ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [Commute, SemiconjBy, inv_mul, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) = a
⊢ (↑u⁻¹ : α) * a = 1
have rw : (↑u⁻¹ : α) * (↑u : α) = 1
Tactic: rw [← h, u.inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) = a
rw : (↑u⁻¹ : α) * (↑u : α) = 1
⊢ (↑u⁻¹ : α) * a = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← h, u.inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) = a
⊢ a * (↑u⁻¹ : α) = 1
have rw : (↑u : α) * (↑u⁻¹ : α) = 1
Tactic: rw [← h, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) = a
rw : (↑u : α) * (↑u⁻¹ : α) = 1
⊢ a * (↑u⁻¹ : α) = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← h, u.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b : α
⊢ (↑a : α) * ((↑a⁻¹ : α) * b) = b
have rw : (↑a : α) * (↑a⁻¹ : α) * b = b
Tactic: rw [← mul_assoc, mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b : α
rw : (↑a : α) * (↑a⁻¹ : α) * b = b
⊢ (↑a : α) * ((↑a⁻¹ : α) * b) = b
have rw₁ : 1 * b = b
Tactic: rw [← mul_assoc, mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b : α
rw : (↑a : α) * (↑a⁻¹ : α) * b = b
rw₁ : 1 * b = b
⊢ (↑a : α) * ((↑a⁻¹ : α) * b) = b
have rw₂ : b = b
Tactic: rw [← mul_assoc, mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b : α
⊢ (↑a⁻¹ : α) * ((↑a : α) * b) = b
have rw : (↑a⁻¹ : α) * (↑a : α) * b = b
Tactic: rw [← mul_assoc, inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b : α
rw : (↑a⁻¹ : α) * (↑a : α) * b = b
⊢ (↑a⁻¹ : α) * ((↑a : α) * b) = b
have rw₁ : 1 * b = b
Tactic: rw [← mul_assoc, inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b : α
rw : (↑a⁻¹ : α) * (↑a : α) * b = b
rw₁ : 1 * b = b
⊢ (↑a⁻¹ : α) * ((↑a : α) * b) = b
have rw₂ : b = b
Tactic: rw [← mul_assoc, inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b c : α
h : (↑a⁻¹ : α) * b = c
⊢ b = (↑a : α) * c
have rw : b = (↑a : α) * ((↑a⁻¹ : α) * b)
Tactic: rw [← h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b c : α
h : (↑a⁻¹ : α) * b = c
rw : b = (↑a : α) * ((↑a⁻¹ : α) * b)
⊢ b = (↑a : α) * c
have rw₁ : b = b
Tactic: rw [← h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b c : α
h : b = (↑a : α) * c
⊢ (↑a⁻¹ : α) * b = c
have rw : (↑a⁻¹ : α) * ((↑a : α) * c) = c
Tactic: rw [h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : αˣ
b c : α
h : b = (↑a : α) * c
rw : (↑a⁻¹ : α) * ((↑a : α) * c) = c
⊢ (↑a⁻¹ : α) * b = c
have rw₁ : c = c
Tactic: rw [h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
⊢ (↑a : α) ^ n * (↑a⁻¹ : α) ^ n = 1
have rw : ((↑a : α) * (↑a⁻¹ : α)) ^ n = 1
Tactic: rw [← a.commute_coe_inv.mul_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
⊢ (↑a⁻¹ : α) ^ n * (↑a : α) ^ n = 1
have rw : ((↑a⁻¹ : α) * (↑a : α)) ^ n = 1
Tactic: rw [← a.commute_inv_coe.mul_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b u a : αˣ
⊢ { val := HPow.hPow (β := ℕ) (↑a : α) 0, inv := HPow.hPow (β := ℕ) (↑a⁻¹ : α) 0, val_inv := ⋯, inv_val := ⋯ : αˣ } = 1
have huv : (↑{ val := HPow.hPow (β := ℕ) (↑a : α) 0, inv := HPow.hPow (β := ℕ) (↑a⁻¹ : α) 0, val_inv := sorry, inv_val := sorry : αˣ } :
    α) =
  (↑1 : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
⊢ { val := (↑a : α) ^ (n + 1), inv := (↑a⁻¹ : α) ^ (n + 1), val_inv := ⋯, inv_val := ⋯ : αˣ } =
    { val := (↑a : α) ^ n, inv := (↑a⁻¹ : α) ^ n, val_inv := ⋯, inv_val := ⋯ : αˣ } * a
have huv : (↑{ val := (↑a : α) ^ (n + 1), inv := (↑a⁻¹ : α) ^ (n + 1), val_inv := sorry, inv_val := sorry : αˣ } : α) =
  (↑({ val := (↑a : α) ^ n, inv := (↑a⁻¹ : α) ^ n, val_inv := sorry, inv_val := sorry : αˣ } * a) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
⊢ (↑a : α) * (↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α)) = 1
have rw : (↑a : α) * ((↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α))) = 1
Tactic: rw [mul_assoc, inv_mul_cancel_left, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
rw : (↑a : α) * ((↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α))) = 1
⊢ (↑a : α) * (↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α)) = 1
have rw₁ : (↑a : α) * (↑a⁻¹ : α) = 1
Tactic: rw [mul_assoc, inv_mul_cancel_left, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
rw : (↑a : α) * ((↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α))) = 1
rw₁ : (↑a : α) * (↑a⁻¹ : α) = 1
⊢ (↑a : α) * (↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α)) = 1
have rw₂ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [mul_assoc, inv_mul_cancel_left, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
⊢ (↑b : α) * (↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α)) = 1
have rw : (↑b : α) * ((↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α))) = 1
Tactic: rw [mul_assoc, inv_mul_cancel_left, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
rw : (↑b : α) * ((↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α))) = 1
⊢ (↑b : α) * (↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α)) = 1
have rw₁ : (↑b : α) * (↑b⁻¹ : α) = 1
Tactic: rw [mul_assoc, inv_mul_cancel_left, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
rw : (↑b : α) * ((↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α))) = 1
rw₁ : (↑b : α) * (↑b⁻¹ : α) = 1
⊢ (↑b : α) * (↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α)) = 1
have rw₂ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [mul_assoc, inv_mul_cancel_left, mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
⊢ a * ((↑u⁻¹ : α) * (↑u : α)) = a
have rw : a * 1 = a
Tactic: rw [Units.inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
rw : a * 1 = a
⊢ a * ((↑u⁻¹ : α) * (↑u : α)) = a
have rw₁ : a = a
Tactic: rw [Units.inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
⊢ a * ((↑u : α) * (↑u⁻¹ : α)) = a
have rw : a * 1 = a
Tactic: rw [Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
rw : a * 1 = a
⊢ a * ((↑u : α) * (↑u⁻¹ : α)) = a
have rw₁ : a = a
Tactic: rw [Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
⊢ (↑u⁻¹ : α) = 1 /ₚ u
have rw : (↑u⁻¹ : α) = (↑u⁻¹ : α)
Tactic: rw [one_divp]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
⊢ (↑(u₁ / u₂) : α) = (↑u₁ : α) /ₚ u₂
have rw : (↑(u₁ / u₂) : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
Tactic: rw [divp, division_def, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑(u₁ / u₂) : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
⊢ (↑(u₁ / u₂) : α) = (↑u₁ : α) /ₚ u₂
have rw₁ : (↑(u₁ * u₂⁻¹) : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
Tactic: rw [divp, division_def, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑(u₁ / u₂) : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
rw₁ : (↑(u₁ * u₂⁻¹) : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
⊢ (↑(u₁ / u₂) : α) = (↑u₁ : α) /ₚ u₂
have rw₂ : (↑u₁ : α) * (↑u₂⁻¹ : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
Tactic: rw [divp, division_def, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
⊢ IsUnit x ↔ ∃ (b : M), x * b = 1 ∧ b * x = 1
have refine : IsUnit x → ∀ (u : Mˣ) (hu : (↑u : M) = x), ∃ (b : M), x * b = 1 ∧ b * x = 1
Tactic: refine ⟨fun ⟨u, hu⟩ => ?_, fun ⟨b, h1b, h2b⟩ => ⟨⟨x, b, h1b, h2b⟩, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
h : IsUnit x
u : Mˣ
hu : (↑u : M) = x
⊢ ∃ (b : M), x * b = 1 ∧ b * x = 1
have subst : IsUnit (↑u : M) → ∃ (b : M), (↑u : M) * b = 1 ∧ b * (↑u : M) = 1
Tactic: subst x
Cleared hypotheses: x, h, hu
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
⊢ ∃ (b : M), a * b = 1
have rcases : ∀ (a b : M) (hab : a * b = 1) (inv_val : b * a = 1),
  ∃ (b_1 : M), (↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val : Mˣ } : M) * b_1 = 1
Tactic: rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
⊢ ∃ (b : M), b * a = 1
have rcases : ∀ (a b : M) (val_inv : a * b = 1) (hba : b * a = 1),
  ∃ (b_1 : M), b_1 * (↑{ val := a, inv := b, val_inv := val_inv, inv_val := hba : Mˣ } : M) = 1
Tactic: rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : IsUnit (a * (↑u : M))
v : Mˣ
hv : (↑v : M) = a * (↑u : M)
⊢ IsUnit (a * (↑u : M) * (↑u⁻¹ : M))
have exists : (↑(v * u⁻¹) : M) = a * (↑u : M) * (↑u⁻¹ : M)
Tactic: exists v * u⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : IsUnit (a * (↑u : M))
v : Mˣ
hv : (↑v : M) = a * (↑u : M)
⊢ (↑(v * u⁻¹) : M) = a * (↑u : M) * (↑u⁻¹ : M)
have rw : (↑(v * u⁻¹) : M) = (↑v : M) * (↑u⁻¹ : M)
Tactic: rw [← hv, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : IsUnit (a * (↑u : M))
v : Mˣ
hv : (↑v : M) = a * (↑u : M)
rw : (↑(v * u⁻¹) : M) = (↑v : M) * (↑u⁻¹ : M)
⊢ (↑(v * u⁻¹) : M) = a * (↑u : M) * (↑u⁻¹ : M)
have rw₁ : (↑v : M) * (↑u⁻¹ : M) = (↑v : M) * (↑u⁻¹ : M)
Tactic: rw [← hv, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (hypothesis)
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : IsUnit (a * (↑u : M))
v : Mˣ
hv : (↑v : M) = a * (↑u : M)
⊢ IsUnit a
have this : IsUnit (a * (↑u : M) * (↑u⁻¹ : M))
Tactic: have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : IsUnit (a * (↑u : M))
v : Mˣ
hv : (↑v : M) = a * (↑u : M)
this : IsUnit (a * (↑u : M) * (↑u⁻¹ : M))
⊢ IsUnit a
have rwa : ∀ (this : IsUnit (a * ((↑u : M) * (↑u⁻¹ : M)))), IsUnit a
Tactic: rwa [mul_assoc, Units.mul_inv, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : IsUnit (a * (↑u : M))
v : Mˣ
hv : (↑v : M) = a * (↑u : M)
this : IsUnit (a * (↑u : M) * (↑u⁻¹ : M))
rwa : ∀ (this : IsUnit (a * ((↑u : M) * (↑u⁻¹ : M)))), IsUnit a
⊢ IsUnit a
have rwa₁ : ∀ (this : IsUnit (a * 1)), IsUnit a
Tactic: rwa [mul_assoc, Units.mul_inv, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : IsUnit (a * (↑u : M))
v : Mˣ
hv : (↑v : M) = a * (↑u : M)
this : IsUnit (a * (↑u : M) * (↑u⁻¹ : M))
rwa : ∀ (this : IsUnit (a * ((↑u : M) * (↑u⁻¹ : M)))), IsUnit a
rwa₁ : ∀ (this : IsUnit (a * 1)), IsUnit a
⊢ IsUnit a
have rwa₂ : ∀ (this : IsUnit a), IsUnit a
Tactic: rwa [mul_assoc, Units.mul_inv, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
a : M
h : IsUnit ((↑u : M) * a)
v : Mˣ
hv : (↑v : M) = (↑u : M) * a
⊢ IsUnit ((↑u⁻¹ : M) * ((↑u : M) * a))
have exists : (↑(u⁻¹ * v) : M) = (↑u⁻¹ : M) * ((↑u : M) * a)
Tactic: exists u⁻¹ * v
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
a : M
h : IsUnit ((↑u : M) * a)
v : Mˣ
hv : (↑v : M) = (↑u : M) * a
⊢ (↑(u⁻¹ * v) : M) = (↑u⁻¹ : M) * ((↑u : M) * a)
have rw : (↑(u⁻¹ * v) : M) = (↑u⁻¹ : M) * (↑v : M)
Tactic: rw [← hv, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
a : M
h : IsUnit ((↑u : M) * a)
v : Mˣ
hv : (↑v : M) = (↑u : M) * a
rw : (↑(u⁻¹ * v) : M) = (↑u⁻¹ : M) * (↑v : M)
⊢ (↑(u⁻¹ * v) : M) = (↑u⁻¹ : M) * ((↑u : M) * a)
have rw₁ : (↑u⁻¹ : M) * (↑v : M) = (↑u⁻¹ : M) * (↑v : M)
Tactic: rw [← hv, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (hypothesis)
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
a : M
h : IsUnit ((↑u : M) * a)
v : Mˣ
hv : (↑v : M) = (↑u : M) * a
⊢ IsUnit a
have this : IsUnit ((↑u⁻¹ : M) * ((↑u : M) * a))
Tactic: have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
a : M
h : IsUnit ((↑u : M) * a)
v : Mˣ
hv : (↑v : M) = (↑u : M) * a
this : IsUnit ((↑u⁻¹ : M) * ((↑u : M) * a))
⊢ IsUnit a
have rwa : ∀ (this : IsUnit ((↑u⁻¹ : M) * (↑u : M) * a)), IsUnit a
Tactic: rwa [← mul_assoc, Units.inv_mul, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
a : M
h : IsUnit ((↑u : M) * a)
v : Mˣ
hv : (↑v : M) = (↑u : M) * a
this : IsUnit ((↑u⁻¹ : M) * ((↑u : M) * a))
rwa : ∀ (this : IsUnit ((↑u⁻¹ : M) * (↑u : M) * a)), IsUnit a
⊢ IsUnit a
have rwa₁ : ∀ (this : IsUnit (1 * a)), IsUnit a
Tactic: rwa [← mul_assoc, Units.inv_mul, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
a : M
h : IsUnit ((↑u : M) * a)
v : Mˣ
hv : (↑v : M) = (↑u : M) * a
this : IsUnit ((↑u⁻¹ : M) * ((↑u : M) * a))
rwa : ∀ (this : IsUnit ((↑u⁻¹ : M) * (↑u : M) * a)), IsUnit a
rwa₁ : ∀ (this : IsUnit (1 * a)), IsUnit a
⊢ IsUnit a
have rwa₂ : ∀ (this : IsUnit a), IsUnit a
Tactic: rwa [← mul_assoc, Units.inv_mul, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
⊢ a * (↑h.unit⁻¹ : M) = 1
have rw : a * (↑h.unit⁻¹ : M) = (↑h.unit : M) * (↑h.unit⁻¹ : M)
Tactic: rw [← h.unit.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
u : αˣ
⊢ (↑u : α)⁻¹ * (↑u : α) = 1
have rw : (↑u⁻¹ : α) * (↑u : α) = 1
Tactic: rw [← Units.val_inv_eq_inv_val, Units.inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
u : αˣ
rw : (↑u⁻¹ : α) * (↑u : α) = 1
⊢ (↑u : α)⁻¹ * (↑u : α) = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← Units.val_inv_eq_inv_val, Units.inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
u : αˣ
⊢ (↑u : α) * (↑u : α)⁻¹ = 1
have rw : (↑u : α) * (↑u⁻¹ : α) = 1
Tactic: rw [← Units.val_inv_eq_inv_val, Units.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
u : αˣ
rw : (↑u : α) * (↑u⁻¹ : α) = 1
⊢ (↑u : α) * (↑u : α)⁻¹ = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← Units.val_inv_eq_inv_val, Units.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ a / a = 1
have rw : a * a⁻¹ = 1
Tactic: rw [div_eq_mul_inv, h.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
rw : a * a⁻¹ = 1
⊢ a / a = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [div_eq_mul_inv, h.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ IsUnit a⁻¹
have obtain : ∀ (u : αˣ) (hu : (↑u : α) = a), IsUnit a⁻¹
Tactic: obtain ⟨u, hu⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
hu : (↑u : α) = a
⊢ IsUnit a⁻¹
have rw : IsUnit (↑u⁻¹ : α)
Tactic: rw [← hu, ← Units.val_inv_eq_inv_val]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)
have rw : IsUnit (a * b⁻¹)
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ b / (a * b) = a⁻¹
have rw : b * (a * b)⁻¹ = a⁻¹
Tactic: rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
rw : b * (a * b)⁻¹ = a⁻¹
⊢ b / (a * b) = a⁻¹
have rw₁ : b * (b⁻¹ * a⁻¹) = a⁻¹
Tactic: rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
rw : b * (a * b)⁻¹ = a⁻¹
rw₁ : b * (b⁻¹ * a⁻¹) = a⁻¹
⊢ b / (a * b) = a⁻¹
have rw₂ : a⁻¹ = a⁻¹
Tactic: rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = b⁻¹
have rw : a / (b * a) = b⁻¹
Tactic: rw [mul_comm, h.div_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : a / (b * a) = b⁻¹
⊢ a / (a * b) = b⁻¹
have rw₁ : b⁻¹ = b⁻¹
Tactic: rw [mul_comm, h.div_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
⊢ c * a / (c * b) = a / b
have rw : a * c / (c * b) = a / b
Tactic: rw [mul_comm c, mul_comm c, h.mul_div_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
rw : a * c / (c * b) = a / b
⊢ c * a / (c * b) = a / b
have rw₁ : a * c / (b * c) = a / b
Tactic: rw [mul_comm c, mul_comm c, h.mul_div_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
rw : a * c / (c * b) = a / b
rw₁ : a * c / (b * c) = a / b
⊢ c * a / (c * b) = a / b
have rw₂ : a / b = a / b
Tactic: rw [mul_comm c, mul_comm c, h.mul_div_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a / (↑u : α)
have rw : a /ₚ u = a * (↑u : α)⁻¹
Tactic: rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
rw : a /ₚ u = a * (↑u : α)⁻¹
⊢ a /ₚ u = a / (↑u : α)
have rw₁ : a * (↑u⁻¹ : α) = a * (↑u : α)⁻¹
Tactic: rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
rw : a /ₚ u = a * (↑u : α)⁻¹
rw₁ : a * (↑u⁻¹ : α) = a * (↑u : α)⁻¹
⊢ a /ₚ u = a / (↑u : α)
have rw₂ : a * (↑u : α)⁻¹ = a * (↑u : α)⁻¹
Tactic: rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1
have change : (↑sorry.unit⁻¹ : M) * a = 1
Tactic: change ↑(h a).unit⁻¹ * a = 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ (↑⋯.unit⁻¹ : M) * a = 1
have rw : a = (↑sorry.unit : M) * 1
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
rw : a = (↑⋯.unit : M) * 1
⊢ (↑⋯.unit⁻¹ : M) * a = 1
have rw₁ : a = a * 1
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
rw : a = (↑⋯.unit : M) * 1
rw₁ : a = a * 1
⊢ (↑⋯.unit⁻¹ : M) * a = 1
have rw₂ : a = a
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1
have change : (↑sorry.unit⁻¹ : M) * a = 1
Tactic: change ↑(h a).unit⁻¹ * a = 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ (↑⋯.unit⁻¹ : M) * a = 1
have rw : a = (↑sorry.unit : M) * 1
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
rw : a = (↑⋯.unit : M) * 1
⊢ (↑⋯.unit⁻¹ : M) * a = 1
have rw₁ : a = a * 1
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]