awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤ
h : u = 1 ∨ u = -1
inl : IsUnit (M := ℤ) 1
inr : IsUnit (M := ℤ) (-1)
⊢ IsUnit u

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
⊢ IsUnit (M := ℤ) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
⊢ IsUnit (M := ℤ) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
⊢ HMul.hMul (α := ℤ) (-1) (-1) = 1

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
⊢ IsUnit (M := ℤ) (-1)

Tactic:
exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u * v = 1
⊢ u = 1 ∨ u = -1

Tactic:
isUnit_iff.1 (.of_mul_eq_one v h)

Premises used: IsUnit.of_mul_eq_one, Iff.mp, Int.isUnit_iff
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u * v = 1
⊢ v * u = 1

Tactic:
have h' : v * u = 1 := mul_comm u v ▸ h
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u * v = 1
h' : v * u = 1
inl : ∀ (h : 1 * v = 1) (h' : v * 1 = 1), Eq (α := ℤ) 1 1 ∧ v = 1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = -1
inr : ∀ (h : -1 * v = 1) (h' : v * -1 = 1), Eq (α := ℤ) (-1) 1 ∧ v = 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = -1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h

Premises used: Int.eq_one_or_neg_one_of_mul_eq_one, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
v : ℤ
h : 1 * v = 1
h' : v * 1 = 1
inl : ∀ (h h' : HMul.hMul (α := ℤ) 1 1 = 1), Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)
inl₁ :
  ∀ (h : HMul.hMul (α := ℤ) 1 (-1) = 1) (h' : HMul.hMul (α := ℤ) (-1) 1 = 1),
    Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) (-1) (-1)
⊢ Eq (α := ℤ) 1 1 ∧ v = 1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = -1

Tactic:
obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h'

Premises used: Int.eq_one_or_neg_one_of_mul_eq_one, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
v : ℤ
h : -1 * v = 1
h' : v * -1 = 1
inr :
  ∀ (h : HMul.hMul (α := ℤ) (-1) 1 = 1) (h' : HMul.hMul (α := ℤ) 1 (-1) = 1),
    Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) 1 (-1)
inr₁ :
  ∀ (h h' : HMul.hMul (α := ℤ) (-1) (-1) = 1),
    Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)
⊢ Eq (α := ℤ) (-1) 1 ∧ v = 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = -1

Tactic:
obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h'

Premises used: Int.eq_one_or_neg_one_of_mul_eq_one, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h h' : HMul.hMul (α := ℤ) 1 1 = 1
inl inl₁ : ¬(Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1) → Eq (α := ℤ) 1 (-1)
inl₂ inl₃ inl₄ inl₅ : ¬Eq (α := ℤ) 1 1 → Eq (α := ℤ) 1 (-1)
⊢ Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h : HMul.hMul (α := ℤ) 1 (-1) = 1
h' : HMul.hMul (α := ℤ) (-1) 1 = 1
⊢ Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) (-1) (-1)

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h : HMul.hMul (α := ℤ) (-1) 1 = 1
h' : HMul.hMul (α := ℤ) 1 (-1) = 1
⊢ Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) 1 (-1)

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h h' : HMul.hMul (α := ℤ) (-1) (-1) = 1
inr inr₁ : ¬(Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1) → Eq (α := ℤ) (-1) (-1)
inr₂ inr₃ inr₄ inr₅ inr₆ inr₇ inr₈ inr₉ inr₁₀ inr₁₁ inr₁₂ inr₁₃ inr₁₄ inr₁₅ inr₁₆ inr₁₇ inr₁₈ inr₁₉ inr₂₀ inr₂₁ inr₂₂ inr₂₃ inr₂₄ inr₂₅ inr₂₆ inr₂₇ inr₂₈ inr₂₉ :
  ¬Eq (α := ℤ) (-1) 1 → Eq (α := ℤ) (-1) (-1)
⊢ Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u * v = 1
⊢ u = v

Tactic:
(eq_one_or_neg_one_of_mul_eq_one' h).elim
    (and_imp.2 (·.trans ·.symm)) (and_imp.2 (·.trans ·.symm))

Premises used: Iff.mpr, and_imp, Int.eq_one_or_neg_one_of_mul_eq_one', Or.elim, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
⊢ u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩

Premises used: Int.eq_one_or_neg_one_of_mul_eq_one', Iff.intro, Or.elim
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
refine_1 : ∀ (h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1) (H : u = 1 ∧ v = 1), u * v = 1
refine_2 : ∀ (h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1) (H : u = -1 ∧ v = -1), u * v = 1
⊢ u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = 1 ∧ v = 1
refine_1 :
  ∀ (h : Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)), HMul.hMul (α := ℤ) 1 1 = 1
⊢ u * v = 1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = -1 ∧ v = -1
refine_2 :
  ∀ (h : Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)),
    HMul.hMul (α := ℤ) (-1) (-1) = 1
⊢ u * v = 1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h : Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)
⊢ HMul.hMul (α := ℤ) 1 1 = 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h : Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)
⊢ HMul.hMul (α := ℤ) (-1) (-1) = 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u * v = -1
inl : ∀ (h : 1 * v = -1), Eq (α := ℤ) 1 1 ∧ v = -1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = 1
inr : ∀ (h : -1 * v = -1), Eq (α := ℤ) (-1) 1 ∧ v = -1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = 1
⊢ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1

Premises used: IsUnit.mul_iff, Iff.mpr, Int.isUnit_eq_one_or, And.left, Iff.mp, Int.isUnit_iff, Or.inr, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
v : ℤ
h : 1 * v = -1
⊢ Eq (α := ℤ) 1 1 ∧ v = -1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = 1

Tactic:
Or.inl ⟨rfl, one_mul v ▸ h⟩

Premises used: Eq.rec, And.intro, Or.inl, one_mul, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
v : ℤ
h : 1 * v = -1
⊢ Eq (α := ℤ) 1 1 ∧ v = -1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = 1

Tactic:
exact Or.inl ⟨rfl, one_mul v ▸ h⟩

Premises used: Or.inl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
v : ℤ
h : -1 * v = -1
⊢ Eq (α := ℤ) (-1) 1 ∧ v = -1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = 1

Tactic:
simpa [Int.neg_mul] using h

Premises used: Int.neg_mul
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩

Premises used: Int.eq_one_or_neg_one_of_mul_eq_neg_one', Iff.intro, Or.elim
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
refine_1 : ∀ (h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1) (H : u = 1 ∧ v = -1), u * v = -1
refine_2 : ∀ (h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1) (H : u = -1 ∧ v = 1), u * v = -1
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = 1 ∧ v = -1
refine_1 :
  ∀ (h : Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) (-1) (-1) ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) (-1) 1),
    HMul.hMul (α := ℤ) 1 (-1) = -1
⊢ u * v = -1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = -1 ∧ v = 1
refine_2 :
  ∀ (h : Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) 1 (-1) ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) 1 1),
    HMul.hMul (α := ℤ) (-1) 1 = -1
⊢ u * v = -1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h : Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) (-1) (-1) ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) (-1) 1
⊢ HMul.hMul (α := ℤ) 1 (-1) = -1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
h : Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) 1 (-1) ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) 1 1
⊢ HMul.hMul (α := ℤ) (-1) 1 = -1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤ
⊢ IsUnit u ↔ u.natAbs = 1

Tactic:
simp [natAbs_eq_iff, isUnit_iff]

Premises used: Int.natAbs_eq_iff, Int.isUnit_iff
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
n : ℕ
⊢ IsUnit (M := ℤ) (↑n : ℤ) ↔ IsUnit n

Tactic:
simp [isUnit_iff_natAbs_eq]

Premises used: Int.isUnit_iff_natAbs_eq
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤ
hu : IsUnit u
⊢ u * u = 1

Tactic:
(isUnit_eq_one_or hu).elim (fun h ↦ h.symm ▸ rfl) fun h ↦ h.symm ▸ rfl

Premises used: Int.isUnit_eq_one_or, Eq.rec, Or.elim, Eq.symm, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a = 1 ∨ a = -1

Tactic:
rw [isUnit_iff] at ha hb hc hd

Premises used: Int.isUnit_iff
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
ha₁ : a = 1 ∨ a = -1
⊢ b = 1 ∨ b = -1

Tactic:
rw [isUnit_iff] at ha hb hc hd

Premises used: Int.isUnit_iff
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
ha₁ : a = 1 ∨ a = -1
hb₁ : b = 1 ∨ b = -1
⊢ c = 1 ∨ c = -1

Tactic:
rw [isUnit_iff] at ha hb hc hd

Premises used: Int.isUnit_iff
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
ha₁ : a = 1 ∨ a = -1
hb₁ : b = 1 ∨ b = -1
hc₁ : c = 1 ∨ c = -1
⊢ d = 1 ∨ d = -1

Tactic:
rw [isUnit_iff] at ha hb hc hd

Premises used: Int.isUnit_iff
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
a b c d : ℤ
ha : a = 1 ∨ a = -1
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
h : u * v = -1
⊢ u = 1 ∨ u = -1

Tactic:
Or.elim (eq_one_or_neg_one_of_mul_eq_neg_one' h) (fun H => Or.inl H.1) fun H => Or.inr H.1

Premises used: And.left, Int.eq_one_or_neg_one_of_mul_eq_neg_one', Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a : α
inst_1 : Invertible a
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a : α
inst_1 : Invertible a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * a = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a : α
inst_1 : Invertible a
⊢ IsUnit a

Tactic:
⟨unitOfInvertible a, rfl⟩

Premises used: IsUnit, Exists.intro, unitOfInvertible, rfl
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
inst_1 : Invertible (↑u : α)
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑u : α) _ = (↑u⁻¹ : α)

Tactic:
invOf_eq_right_inv u.mul_inv

Premises used: invOf_eq_right_inv, Units.mul_inv
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a : α
h : IsUnit a
⊢ Nonempty.{u + 1} (Invertible a)

Tactic:
let ⟨x, hx⟩ := h
  ⟨x.invertible.copy _ hx.symm⟩

Premises used: Nonempty.intro, Invertible, Nonempty, Units.invertible, Eq.symm, Invertible.copy, _private.0.IsUnit.nonempty_invertible.match_1
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a : α
⊢ Nonempty.{u + 1} (Invertible a) ↔ IsUnit a

Tactic:
⟨Nonempty.rec <| @isUnit_of_invertible _ _ _, IsUnit.nonempty_invertible⟩

Premises used: IsUnit.nonempty_invertible, Nonempty.rec, Iff.intro
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute a b
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute a b
rw rw₁ :
  @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)

Tactic:
rw [h.eq]

Premises used: Commute.eq
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute a b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * a

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute b a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * a =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute b a
rw rw₁ :
  @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)

Tactic:
rw [h.eq]

Premises used: Commute.eq
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute b a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
M : Type u_1
inst : One M
inst_1 : Mul M
m : M
inst_2 : Invertible m
⊢ Commute m (@Invertible.invOf _ inst_1 inst m _)

Tactic:
calc
    m * ⅟m = 1 := mul_invOf_self m
    _ = ⅟m * m := (invOf_mul_self m).symm

Premises used: Trans.trans, SemiconjBy, Commute, invOf_mul_self, mul_invOf_self, Eq.symm
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1

Tactic:
rw [mul_assoc, invOf_mul_self]

Premises used: mul_assoc, invOf_mul_self
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : a * (b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a)) = a * 1
rw₁ : a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = a * 1
rw₂ : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = a * 1
rw₃ : 1 * a = a * 1
rw₄ : 1 * a = a
rw₅ rw₆ : a = a
⊢ b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = 1

Tactic:
rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]

Premises used: isUnit_of_invertible, mul_assoc, mul_invOf_self, IsUnit.mul_right_inj, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1 * b
rw₁ : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1 * b
rw₂ : b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b)) = 1 * b
rw₃ : b * 1 = 1 * b
rw₄ : b = 1 * b
rw₅ rw₆ : b = b
⊢ b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = 1

Tactic:
rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]

Premises used: isUnit_of_invertible, mul_assoc, invOf_mul_self, IsUnit.mul_left_inj, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ a * (b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _) = 1

Tactic:
rw [← mul_assoc, mul_invOf_self]

Premises used: mul_assoc, mul_invOf_self
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne m _ * m) ^ n = 1
rw₁ : HPow.hPow (α := α) 1 n = 1
rw₂ rw₃ : Eq.{u + 1} (α := α) 1 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n * m ^ n = 1

Tactic:
rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]

Premises used: one_pow, commute_invOf, invOf_mul_self, Commute.symm, Commute.mul_pow
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
rw : (m * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _) ^ n = 1
rw₁ : HPow.hPow (α := α) 1 n = 1
rw₂ rw₃ : Eq.{u + 1} (α := α) 1 1
⊢ m ^ n * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n = 1

Tactic:
rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]

Premises used: one_pow, commute_invOf, mul_invOf_self, Commute.mul_pow
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
inst_2 : Invertible (m ^ n)
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne (m ^ n) _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n

Tactic:
@invertible_unique _ _ _ _ _ (invertiblePow m n) rfl

Premises used: invertible_unique, rfl
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _ * r) : S) (1 : S)
rw₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) 1 1
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S)
      ((f : (a : R) → S) r : S) =
    1

Tactic:
rw [← map_mul, invOf_mul_self, map_one]

Premises used: Invertible.invOf_mul_self, map_mul, map_one
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (r * @invOf _ MulOne.toMul MulOne.toOne r _) : S) (1 : S)
rw₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) 1 1
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) r : S)
      ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S) =
    1

Tactic:
rw [← map_mul, mul_invOf_self, map_one]

Premises used: Invertible.mul_invOf_self, map_mul, map_one
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
ifr : Invertible (α := S) ((f : (a : R) → S) r : S)
⊢ ifr = Invertible.map f r

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
ifr : Invertible (α := S) ((f : (a : R) → S) r : S)
obtain :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@Invertible.invOf _ MulOne.toMul MulOne.toOne r _) : S)
    (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((f : (a : R) → S) r) _ : S)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@Invertible.invOf _ MulOne.toMul MulOne.toOne r _) : S)
    (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((f : (a : R) → S) r) _ : S)

Tactic:
obtain rfl : ifr = Invertible.map f r := Subsingleton.elim _ _

Premises used: Invertible.map, Subsingleton.elim, rfl
-- Module: Mathlib.Algebra.Group.Invertible.Basic
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@Invertible.invOf _ MulOne.toMul MulOne.toOne r _) : S)
    (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((f : (a : R) → S) r) _ : S)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : One α
a : α
x : Invertible a
⊢ @Invertible.invOf _ inst inst_1 a _ * a = 1

Tactic:
Invertible.invOf_mul_self

Premises used: Invertible.invOf_mul_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : One α
a : α
inst_2 : Invertible a
⊢ @Invertible.invOf _ inst inst_1 a _ * a = 1

Tactic:
invOf_mul_self' _

Premises used: invOf_mul_self'
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : One α
a : α
x : Invertible a
⊢ a * @Invertible.invOf _ inst inst_1 a _ = 1

Tactic:
Invertible.mul_invOf_self

Premises used: Invertible.mul_invOf_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : One α
a : α
inst_2 : Invertible a
⊢ a * @Invertible.invOf _ inst inst_1 a _ = 1

Tactic:
mul_invOf_self' _

Premises used: mul_invOf_self'
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * a * b = b
rw₁ : 1 * b = b
rw₂ rw₃ : b = b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * (a * b) = b

Tactic:
rw [← mul_assoc, invOf_mul_self, one_mul]

Premises used: mul_assoc, invOf_mul_self, one_mul
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b_1 : α
G : Type u_1
inst_1 : Group G
a b : G
⊢ a⁻¹ * (a * b) = b

Tactic:
inv_mul_cancel_left a b

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * (a * b) = b

Tactic:
invOf_mul_cancel_left' _ _

Premises used: invOf_mul_cancel_left'
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b = b
rw₁ : 1 * b = b
rw₂ rw₃ : b = b
⊢ a * (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) = b

Tactic:
rw [← mul_assoc, mul_invOf_self, one_mul]

Premises used: mul_assoc, mul_invOf_self, one_mul
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b_1 : α
G : Type u_1
inst_1 : Group G
a b : G
⊢ a * (a⁻¹ * b) = b

Tactic:
mul_inv_cancel_left a b

Premises used: mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
⊢ a * (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) = b

Tactic:
mul_invOf_cancel_left' a b

Premises used: mul_invOf_cancel_left'
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible b
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * b = a

Tactic:
simp [mul_assoc]

Premises used: mul_assoc