awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
huv :
  (↑{ val := (↑a : α) ^ (n + 1), inv := (↑a⁻¹ : α) ^ (n + 1), val_inv := ⋯, inv_val := ⋯ : αˣ } : α) =
    (↑({ val := (↑a : α) ^ n, inv := (↑a⁻¹ : α) ^ n, val_inv := ⋯, inv_val := ⋯ : αˣ } * a) : α)
⊢ { val := (↑a : α) ^ (n + 1), inv := (↑a⁻¹ : α) ^ (n + 1), val_inv := ⋯, inv_val := ⋯ : αˣ } =
    { val := (↑a : α) ^ n, inv := (↑a⁻¹ : α) ^ n, val_inv := ⋯, inv_val := ⋯ : αˣ } * a

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Units.Defs
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) : α)

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
rw : (↑a : α) * ((↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α))) = 1
rw₁ : (↑a : α) * (↑a⁻¹ : α) = 1
rw₂ rw₃ : Eq.{u + 1} (α := α) 1 1
⊢ (↑a : α) * (↑b⁻¹ : α) * ((↑b : α) * (↑a⁻¹ : α)) = 1

Tactic:
rw [mul_assoc, inv_mul_cancel_left, mul_inv]

Premises used: mul_assoc, Units.mul_inv, Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b_1 u a b : αˣ
rw : (↑b : α) * ((↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α))) = 1
rw₁ : (↑b : α) * (↑b⁻¹ : α) = 1
rw₂ rw₃ : Eq.{u + 1} (α := α) 1 1
⊢ (↑b : α) * (↑a⁻¹ : α) * ((↑a : α) * (↑b⁻¹ : α)) = 1

Tactic:
rw [mul_assoc, inv_mul_cancel_left, mul_inv]

Premises used: mul_assoc, Units.mul_inv, Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u a : αˣ
⊢ Eq (α := αˣ)
    (match (motive := ℤ → αˣ → αˣ) 0, a with
      | Int.ofNat n, a => a ^ n
      | Int.negSucc n, a => (a ^ n.succ)⁻¹ :
      αˣ)
    (1 : αˣ)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
⊢ (match (motive := ℤ → αˣ → αˣ) (↑n.succ : ℤ), a with
    | Int.ofNat n, a => a ^ n
    | Int.negSucc n, a => (a ^ n.succ)⁻¹) =
    HMul.hMul (α := αˣ)
      (match (motive := ℤ → αˣ → αˣ) (↑n : ℤ), a with
        | Int.ofNat n, a => a ^ n
        | Int.negSucc n, a => (a ^ n.succ)⁻¹ :
        αˣ)
      a

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
⊢ Eq (α := αˣ)
    (match (motive := ℤ → αˣ → αˣ) Int.negSucc n, a with
      | Int.ofNat n, a => a ^ n
      | Int.negSucc n, a => (a ^ n.succ)⁻¹ :
      αˣ)
    ((match (motive := ℤ → αˣ → αˣ) (↑n.succ : ℤ), a with
        | Int.ofNat n, a => a ^ n
        | Int.negSucc n, a => (a ^ n.succ)⁻¹)⁻¹ :
      αˣ)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : αˣ
n : ℕ
⊢ (↑(a ^ n) : α) = (↑a : α) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : αˣ
n : ℕ
⊢ (↑(a ^ n)⁻¹ : α) = (↑a⁻¹ : α) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
u : αˣ
⊢ (↑u⁻¹ : α) = (↑u : α)⁻¹

Tactic:
Eq.symm <| inv_eq_of_mul_eq_one_right u.mul_inv

Premises used: Units.mul_inv, inv_eq_of_mul_eq_one_right, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
⊢ ∀ (u₁ u₂ : αˣ), (↑(u₁ / u₂) : α) = (↑u₁ : α) / (↑u₂ : α)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : IsDedekindFiniteMonoid α
a b : α
h : a * b = 1
⊢ (↑(mkOfMulEqOne a b h) : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u : αˣ
⊢ (↑u : α) /ₚ u = 1

Tactic:
Units.mul_inv _

Premises used: Units.mul_inv, divp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : α
⊢ a /ₚ 1 = a

Tactic:
mul_one _

Premises used: divp, mul_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
u : αˣ
⊢ a * b /ₚ u = a * (b /ₚ u)

Tactic:
mul_assoc _ _ _

Premises used: mul_assoc, divp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
⊢ a /ₚ u⁻¹ = a * (↑u : α)

Tactic:
rfl

Premises used: divp, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
rw : a * 1 = a
rw₁ rw₂ : a = a
⊢ a * ((↑u⁻¹ : α) * (↑u : α)) = a

Tactic:
rw [Units.inv_mul, mul_one]

Premises used: Units.inv_mul, mul_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
rw : a * 1 = a
rw₁ rw₂ : a = a
⊢ a * ((↑u : α) * (↑u⁻¹ : α)) = a

Tactic:
rw [Units.mul_inv, mul_one]

Premises used: Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
x : α
u₁ u₂ : αˣ
⊢ x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)

Tactic:
simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]

Premises used: mul_assoc, divp, mul_inv_rev, Units.val_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u : αˣ
⊢ 1 /ₚ u = (↑u⁻¹ : α)

Tactic:
one_mul _

Premises used: divp, one_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u : αˣ
rw rw₁ : (↑u⁻¹ : α) = (↑u⁻¹ : α)
⊢ (↑u⁻¹ : α) = 1 /ₚ u

Tactic:
rw [one_divp]

Premises used: one_divp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑(u₁ / u₂) : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
rw₁ : (↑(u₁ * u₂⁻¹) : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
rw₂ rw₃ : (↑u₁ : α) * (↑u₂⁻¹ : α) = (↑u₁ : α) * (↑u₂⁻¹ : α)
⊢ (↑(u₁ / u₂) : α) = (↑u₁ : α) /ₚ u₂

Tactic:
rw [divp, division_def, Units.val_mul]

Premises used: division_def, divp, Units.val_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
x : M
⊢ IsUnit x ↔ ∃ (b : M), x * b = 1 ∧ b * x = 1

Tactic:
⟨fun ⟨u, hu⟩ => ?_, fun ⟨b, h1b, h2b⟩ => ⟨⟨x, b, h1b, h2b⟩, rfl⟩⟩

Premises used: HMul.hMul, IsUnit, _private.0.isUnit_iff_exists.match_2, Exists, And, Iff.intro, Units.mk, Exists.intro, OfNat.ofNat, Eq, rfl, _private.0.isUnit_iff_exists.match_1
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
x : M
refine : IsUnit x → ∀ (u : Mˣ) (hu : (↑u : M) = x), ∃ (b : M), x * b = 1 ∧ b * x = 1
⊢ IsUnit x ↔ ∃ (b : M), x * b = 1 ∧ b * x = 1

Tactic:
refine ⟨fun ⟨u, hu⟩ => ?_, fun ⟨b, h1b, h2b⟩ => ⟨⟨x, b, h1b, h2b⟩, rfl⟩⟩
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
x : M
h : IsUnit x
u : Mˣ
hu : (↑u : M) = x
subst : IsUnit (↑u : M) → ∃ (b : M), (↑u : M) * b = 1 ∧ b * (↑u : M) = 1
⊢ ∃ (b : M), x * b = 1 ∧ b * x = 1

Tactic:
subst x
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
h : IsUnit (↑u : M)
⊢ ∃ (b : M), (↑u : M) * b = 1 ∧ b * (↑u : M) = 1

Tactic:
⟨u.inv, u.val_inv, u.inv_val⟩

Premises used: Units.inv_val, And.intro, Exists.intro, Units.inv, Units.val_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
h : IsUnit (↑u : M)
⊢ ∃ (b : M), (↑u : M) * b = 1 ∧ b * (↑u : M) = 1

Tactic:
exact ⟨u.inv, u.val_inv, u.inv_val⟩
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
⊢ IsUnit a ↔ (∃ (b : M), a * b = 1) ∧ ∃ (c : M), c * a = 1

Tactic:
isUnit_iff_exists.trans
    ⟨fun ⟨b, hba, hab⟩ => ⟨⟨b, hba⟩, ⟨b, hab⟩⟩,
      fun ⟨⟨b, hb⟩, ⟨_, hc⟩⟩ => ⟨b, hb, left_inv_eq_right_inv hc hb ▸ hc⟩⟩

Premises used: isUnit_iff_exists, HMul.hMul, _private.0.isUnit_iff_exists_and_exists.match_1, _private.0.isUnit_iff_exists.match_2, Exists, Eq.rec, left_inv_eq_right_inv, And, And.intro, Iff.intro, Exists.intro, Iff.trans, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
⊢ IsUnit (↑u : M)

Tactic:
⟨u, rfl⟩

Premises used: IsUnit, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
⊢ IsUnit.{u_1} (M := M) 1

Tactic:
⟨1, rfl⟩

Premises used: IsUnit, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsDedekindFiniteMonoid M
a b : M
h : a * b = 1
⊢ IsUnit a

Tactic:
⟨.mkOfMulEqOne a b h, rfl⟩

Premises used: Units.mkOfMulEqOne, IsUnit, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsDedekindFiniteMonoid M
b a : M
h : a * b = 1
⊢ IsUnit b

Tactic:
.of_mul_eq_one a <| mul_eq_one_symm h

Premises used: IsDedekindFiniteMonoid.mul_eq_one_symm, IsUnit.of_mul_eq_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
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
⊢ ∃ (b : M), a * b = 1

Tactic:
rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
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:
⟨b, hab⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
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:
exact ⟨b, hab⟩
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
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
⊢ ∃ (b : M), b * a = 1

Tactic:
rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
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:
⟨b, hba⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
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:
exact ⟨b, hba⟩
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
x y : Mˣ
⊢ IsUnit ((↑x : M) * (↑y : M))

Tactic:
⟨x * y, rfl⟩

Premises used: HMul.hMul, IsUnit, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
x y : Mˣ
⊢ IsUnit ((↑x : M) * (↑y : M))

Tactic:
exact ⟨x * y, rfl⟩
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
u : Mˣ
⊢ IsUnit ((↑u : M) ^ n)

Tactic:
⟨u ^ n, rfl⟩

Premises used: IsUnit, HPow.hPow, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
u : Mˣ
⊢ IsUnit ((↑u : M) ^ n)

Tactic:
exact ⟨u ^ n, rfl⟩
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
h : ∀ (a : M), IsUnit a → a = 1
⊢ Subsingleton.{u_1 + 1} Mˣ

Tactic:
subsingleton_of_forall_eq 1 fun u ↦ Units.ext <| h u u.isUnit

Premises used: Units.val, subsingleton_of_forall_eq, Units.ext, Units.isUnit, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
u : Mˣ
⊢ u = 1

Tactic:
Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
u : Mˣ
⊢ (↑u : M) = 1

Tactic:
simp [u.eq_one]

Premises used: Units.eq_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
⊢ IsUnit.{u_1} (M := M) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
⊢ IsUnit.{u_1} (M := M) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsDedekindFiniteMonoid M
a : M
⊢ IsUnit a ↔ ∃ (b : M), a * b = 1

Tactic:
⟨(·.exists_right_inv), fun ⟨b, hab⟩ ↦ .of_mul_eq_one b hab⟩

Premises used: IsUnit.of_mul_eq_one, IsUnit, _private.0.isUnit_iff_exists_inv.match_1, Iff.intro, IsUnit.exists_right_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsDedekindFiniteMonoid M
a : M
⊢ IsUnit a ↔ ∃ (b : M), b * a = 1

Tactic:
⟨(·.exists_left_inv), fun ⟨b, hba⟩ ↦ .of_mul_eq_one_right b hba⟩

Premises used: _private.0.isUnit_iff_exists_inv'.match_1, IsUnit, IsUnit.of_mul_eq_one_right, IsUnit.exists_left_inv, Iff.intro
-- Module: Mathlib.Algebra.Group.Units.Defs
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)
exists : (↑(v * u⁻¹) : M) = a * (↑u : M) * (↑u⁻¹ : M)
⊢ IsUnit (a * (↑u : M) * (↑u⁻¹ : M))

Tactic:
exists v * u⁻¹
-- Module: Mathlib.Algebra.Group.Units.Defs
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)
rw₁ rw₂ : (↑v : M) * (↑u⁻¹ : M) = (↑v : M) * (↑u⁻¹ : M)
⊢ (↑(v * u⁻¹) : M) = a * (↑u : M) * (↑u⁻¹ : M)

Tactic:
rw [← hv, Units.val_mul]

Premises used: Units.val_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
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))

Tactic:
have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
-- Module: Mathlib.Algebra.Group.Units.Defs
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : IsUnit a), IsUnit a
⊢ IsUnit a

Tactic:
rwa [mul_assoc, Units.mul_inv, mul_one] at this

Premises used: mul_assoc, Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.Group.Units.Defs
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
exists : (↑(u⁻¹ * v) : M) = (↑u⁻¹ : M) * ((↑u : M) * a)
⊢ IsUnit ((↑u⁻¹ : M) * ((↑u : M) * a))

Tactic:
exists u⁻¹ * v
-- Module: Mathlib.Algebra.Group.Units.Defs
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)
rw₁ rw₂ : (↑u⁻¹ : M) * (↑v : M) = (↑u⁻¹ : M) * (↑v : M)
⊢ (↑(u⁻¹ * v) : M) = (↑u⁻¹ : M) * ((↑u : M) * a)

Tactic:
rw [← hv, Units.val_mul]

Premises used: Units.val_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
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))

Tactic:
have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]
-- Module: Mathlib.Algebra.Group.Units.Defs
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : IsUnit a), IsUnit a
⊢ IsUnit a

Tactic:
rwa [← mul_assoc, Units.inv_mul, one_mul] at this

Premises used: mul_assoc, Units.inv_mul, one_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
rwa rwa₁ rwa₂ rwa₃ : x * y * z = 1
⊢ x * (y * z) = 1

Tactic:
rwa [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : z * (x * y) = 1
rwa rwa₁ rwa₂ rwa₃ : z * (x * y) = 1
⊢ z * x * y = 1

Tactic:
rwa [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsDedekindFiniteMonoid M
x y : M
⊢ IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y

Tactic:
⟨fun h => ⟨isUnit_of_mul_isUnit_left h, isUnit_of_mul_isUnit_right h⟩,
   fun h => IsUnit.mul h.1 h.2⟩

Premises used: isUnit_of_mul_isUnit_left, IsUnit.mul, isUnit_of_mul_isUnit_right, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
h : IsUnit (↑a : M)
⊢ h.unit = a

Tactic:
Units.ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
⊢ (↑h.unit : M) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
h : IsUnit.{u_1} (M := M) 1
⊢ h.unit = 1

Tactic:
Units.ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a b : M
ha : IsUnit a
hb : IsUnit b
⊢ ⋯.unit = ha.unit * hb.unit

Tactic:
Units.ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
n : ℕ
⊢ ⋯.unit = h.unit ^ n

Tactic:
Units.ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
⊢ (↑h.unit⁻¹ : M) * a = 1

Tactic:
Units.mul_inv _

Premises used: Units.mul_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
rw : a * (↑h.unit⁻¹ : M) = (↑h.unit : M) * (↑h.unit⁻¹ : M)
⊢ a * (↑h.unit⁻¹ : M) = 1

Tactic:
rw [← h.unit.mul_inv]

Premises used: Units.mul_inv, IsUnit.unit
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
⊢ a * (↑h.unit⁻¹ : M) = (↑h.unit : M) * (↑h.unit⁻¹ : M)

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a b : M
ha : IsUnit a
⊢ IsUnit ((↑ha.unit : M) * b) ↔ IsUnit b

Tactic:
simp [-IsUnit.unit_spec]

Premises used: IsUnit.unit_spec
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
M : Type u_1
inst : Monoid M
a b : M
hb : IsUnit b
⊢ IsUnit (a * (↑hb.unit : M)) ↔ IsUnit a

Tactic:
simp [-IsUnit.unit_spec]

Premises used: IsUnit.unit_spec
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
u : αˣ
rw : (↑u⁻¹ : α) * (↑u : α) = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ (↑u : α)⁻¹ * (↑u : α) = 1

Tactic:
rw [← Units.val_inv_eq_inv_val, Units.inv_mul]

Premises used: Units.val_inv_eq_inv_val, Units.inv_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
u : αˣ
rw : (↑u : α) * (↑u⁻¹ : α) = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ (↑u : α) * (↑u : α)⁻¹ = 1

Tactic:
rw [← Units.val_inv_eq_inv_val, Units.mul_inv]

Premises used: Units.val_inv_eq_inv_val, Units.mul_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ (↑h.unit'⁻¹ : α) = a⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ ∀ (b : α), a * (a⁻¹ * b) = b

Tactic:
h.unit'.mul_inv_cancel_left

Premises used: IsUnit.unit', Units.mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ ∀ (b : α), a⁻¹ * (a * b) = b

Tactic:
h.unit'.inv_mul_cancel_left

Premises used: IsUnit.unit', Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
rw : a * a⁻¹ = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ a / a = 1

Tactic:
rw [div_eq_mul_inv, h.mul_inv_cancel]

Premises used: IsUnit.mul_inv_cancel, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
obtain : ∀ (u : αˣ) (hu : (↑u : α) = a), IsUnit a⁻¹
⊢ IsUnit a⁻¹

Tactic:
obtain ⟨u, hu⟩ := h
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
hu : (↑u : α) = a
rw : IsUnit (↑u⁻¹ : α)
⊢ IsUnit a⁻¹

Tactic:
rw [← hu, ← Units.val_inv_eq_inv_val]

Premises used: Units.val_inv_eq_inv_val
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
hu : (↑u : α) = a
⊢ IsUnit (↑u⁻¹ : α)

Tactic:
Units.isUnit _

Premises used: Units.isUnit
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
hu : (↑u : α) = a
⊢ IsUnit (↑u⁻¹ : α)

Tactic:
exact Units.isUnit _

Premises used: Units.isUnit
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ ⋯.unit = h.unit⁻¹

Tactic:
Units.ext h.unit.val_inv_eq_inv_val.symm

Premises used: Units.val_inv_eq_inv_val, Units.ext, IsUnit.unit, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
rw : IsUnit (a * b⁻¹)
⊢ IsUnit (a / b)

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)

Tactic:
ha.mul hb.inv

Premises used: IsUnit.inv, IsUnit.mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)

Tactic:
exact ha.mul hb.inv

Premises used: IsUnit.inv, IsUnit.mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ ⋯.unit = ha.unit / hb.unit

Tactic:
Units.ext (ha.unit.val_div_eq_div_val hb.unit).symm

Premises used: Units.val_div_eq_div_val, Units.ext, IsUnit.unit, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
rw : b * (a * b)⁻¹ = a⁻¹
rw₁ : b * (b⁻¹ * a⁻¹) = a⁻¹
rw₂ rw₃ : a⁻¹ = a⁻¹
⊢ b / (a * b) = a⁻¹

Tactic:
rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]

Premises used: div_eq_mul_inv, IsUnit.mul_inv_cancel_left, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
c : α
h : IsUnit c
a b : α
⊢ a * c / (b * c) = a / b

Tactic:
simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]

Premises used: mul_assoc, div_eq_mul_inv, IsUnit.mul_inv_cancel_left, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : a / (b * a) = b⁻¹
rw₁ rw₂ : b⁻¹ = b⁻¹
⊢ a / (a * b) = b⁻¹

Tactic:
rw [mul_comm, h.div_mul_cancel_right]

Premises used: IsUnit.div_mul_cancel_right, mul_comm
-- Module: Mathlib.Algebra.Group.Units.Defs
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
rw₂ rw₃ : a / b = a / b
⊢ c * a / (c * b) = a / b

Tactic:
rw [mul_comm c, mul_comm c, h.mul_div_mul_right]

Premises used: IsUnit.mul_div_mul_right, mul_comm
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : DivisionMonoid α
a : α
u : αˣ
rw : a /ₚ u = a * (↑u : α)⁻¹
rw₁ : a * (↑u⁻¹ : α) = a * (↑u : α)⁻¹
rw₂ rw₃ : a * (↑u : α)⁻¹ = a * (↑u : α)⁻¹
⊢ a /ₚ u = a / (↑u : α)

Tactic:
rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]

Premises used: Units.val_inv_eq_inv_val, div_eq_mul_inv, divp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Group α
a : α
⊢ IsUnit a

Tactic:
⟨⟨a, a⁻¹, mul_inv_cancel _, inv_mul_cancel _⟩, rfl⟩

Premises used: inv_mul_cancel, IsUnit, Inv.inv, Units.mk, Exists.intro, mul_inv_cancel, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
change : (↑⋯.unit⁻¹ : M) * a = 1
⊢ a⁻¹ * a = 1

Tactic:
change ↑(h a).unit⁻¹ * a = 1

Premises used: IsUnit.unit
-- Module: Mathlib.Algebra.Group.Units.Defs
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
rw₂ rw₃ : a = a
⊢ (↑⋯.unit⁻¹ : M) * a = 1

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]

Premises used: mul_one, Units.inv_mul_eq_iff_eq_mul, IsUnit.unit_spec