awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
LeftCancelMonoid.eq_one_of_mul_left h

Premises used: LeftCancelMonoid.eq_one_of_mul_left
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ a * b = 1 ↔ a = 1 ∧ b = 1

Tactic:
LeftCancelMonoid.mul_eq_one

Premises used: LeftCancelMonoid.mul_eq_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
LeftCancelMonoid.mul_ne_one

Premises used: LeftCancelMonoid.mul_ne_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
x y : α
u : αˣ
rw : x * (↑u⁻¹ : α) * y = x * y /ₚ u
rw₁ : x * (↑u⁻¹ : α) * y = x * y * (↑u⁻¹ : α)
rw₂ rw₃ : x * y * (↑u⁻¹ : α) = x * y * (↑u⁻¹ : α)
⊢ x /ₚ u * y = x * y /ₚ u

Tactic:
rw [divp, divp, mul_right_comm]

Premises used: divp, mul_right_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
rw : y /ₚ uy * (↑ux : α) = x ↔ x * (↑uy : α) = y * (↑ux : α)
rw₁ : y * (↑ux : α) /ₚ uy = x ↔ x * (↑uy : α) = y * (↑ux : α)
rw₂ rw₃ : x * (↑uy : α) = y * (↑ux : α) ↔ x * (↑uy : α) = y * (↑ux : α)
⊢ x /ₚ ux = y /ₚ uy ↔ x * (↑uy : α) = y * (↑ux : α)

Tactic:
rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]

Premises used: divp_eq_iff_mul_eq, divp_mul_eq_mul_divp
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
x y : α
ux uy : αˣ
rw : x * (y /ₚ uy) /ₚ ux = x * y /ₚ (ux * uy)
rw₁ : x * y /ₚ uy /ₚ ux = x * y /ₚ (ux * uy)
rw₂ rw₃ : x * y /ₚ (ux * uy) = x * y /ₚ (ux * uy)
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)

Tactic:
rw [divp_mul_eq_mul_divp, ← divp_assoc, divp_divp_eq_divp_mul]

Premises used: divp_assoc, divp_mul_eq_mul_divp, divp_divp_eq_divp_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rwa rwa₁ rwa₂ rwa₃ : a * b = 1
⊢ b * a = 1

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
rw : ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Premises used: not_iff_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton M
a : M
⊢ a * a = 1

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
⊢ CanLift M Mˣ Units.val IsUnit

Tactic:
{ prf := fun _ ↦ id }

Premises used: id, CanLift.mk
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton M
x : Mˣ
⊢ (↑x : M) = 1

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : IsUnit a
⊢ b * a = c * a ↔ b = c

Tactic:
let ⟨u, hu⟩ := h
  hu ▸ u.mul_left_inj

Premises used: HMul.hMul, Eq.rec, _private.0.IsUnit.mul_left_inj.match_1, Iff, Units.mul_left_inj, Eq
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : IsUnit a
⊢ a * b = a * c ↔ b = c

Tactic:
let ⟨u, hu⟩ := h
  hu ▸ u.mul_right_inj

Premises used: HMul.hMul, Eq.rec, _private.0.IsUnit.mul_left_inj.match_1, Iff, Units.mul_right_inj, Eq
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : IsUnit a
⊢ a * b = a * c → b = c

Tactic:
h.mul_right_inj.1

Premises used: IsUnit.mul_right_inj, Iff.mp
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : IsUnit b
⊢ a * b = c * b → a = c

Tactic:
h.mul_left_inj.1

Premises used: Iff.mp, IsUnit.mul_left_inj
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit b
rw rw₁ : a * b = b ↔ a * b = b
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit b
rw rw₁ : a = 1 ↔ a = 1
⊢ a * b = 1 * b ↔ a = 1

Tactic:
rw [h.mul_left_inj]

Premises used: IsUnit.mul_left_inj
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit a
rw rw₁ : a * b = a ↔ a * b = a
⊢ a * b = a ↔ a * b = a * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : IsUnit a
rw rw₁ : b = 1 ↔ b = 1
⊢ a * b = a * 1 ↔ b = 1

Tactic:
rw [h.mul_right_inj]

Premises used: IsUnit.mul_right_inj
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
⊢ Injective (β := M) fun (x : M) ↦ a * x

Tactic:
fun _ _ => h.mul_left_cancel

Premises used: IsUnit.mul_left_cancel, Function.Injective
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
b : M
h : IsUnit b
⊢ Injective (β := M) fun (x : M) ↦ x * b

Tactic:
fun _ _ => h.mul_right_cancel

Premises used: Function.Injective, IsUnit.mul_right_cancel
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun (x : M) ↦ a * x) ((↑h.unit⁻¹ : M) * y) = y

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a : M
h : Bijective (β := M) fun (x : M) ↦ a * x
⊢ Eq.{u_1 + 1} (α := M)
    ((fun (x : M) ↦ a * x) (⋯.choose (p := fun (a_1 : M) ↦ Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ a * x) a_1) 1) * a))
    ((fun (x : M) ↦ a * x) 1)

Tactic:
simpa [mul_assoc] using congr_arg (· * a) (h.2 1).choose_spec

Premises used: Exists.choose_spec, HMul.hMul, mul_assoc, congr_arg, And.right, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun (x : M) ↦ x * a) (y * (↑h.unit⁻¹ : M)) = y

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
M : Type u_1
inst : Monoid M
a : M
h : Bijective (β := M) fun (x : M) ↦ x * a
⊢ Eq.{u_1 + 1} (α := M)
    ((fun (x : M) ↦ x * a) (a * ⋯.choose (p := fun (a_1 : M) ↦ Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ x * a) a_1) 1)))
    ((fun (x : M) ↦ x * a) 1)

Tactic:
simpa [mul_assoc] using congr_arg (a * ·) (h.2 1).choose_spec

Premises used: Exists.choose_spec, HMul.hMul, mul_assoc, congr_arg, And.right, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b * b⁻¹ = a

Tactic:
h.unit'.mul_inv_cancel_right _

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

Tactic:
h.unit'.inv_mul_cancel_right _

Premises used: IsUnit.unit', Units.inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b * c⁻¹ ↔ a * c = b

Tactic:
h.unit'.eq_mul_inv_iff_mul_eq

Premises used: IsUnit.unit', Units.eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a = b⁻¹ * c ↔ b * a = c

Tactic:
h.unit'.eq_inv_mul_iff_mul_eq

Premises used: IsUnit.unit', Units.eq_inv_mul_iff_mul_eq
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ a⁻¹ * b = c ↔ b = a * c

Tactic:
h.unit'.inv_mul_eq_iff_eq_mul

Premises used: IsUnit.unit', Units.inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a * b⁻¹ = c ↔ a = c * b

Tactic:
h.unit'.mul_inv_eq_iff_eq_mul

Premises used: IsUnit.unit', Units.mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit b
⊢ a * b⁻¹ = 1 ↔ a = b

Tactic:
@Units.mul_inv_eq_one _ _ h.unit' _

Premises used: Units.mul_inv_eq_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit a
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
@Units.inv_mul_eq_one _ _ h.unit' _

Premises used: Units.inv_mul_eq_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit b
⊢ a * b = 1 ↔ a = b⁻¹

Tactic:
@Units.mul_eq_one_iff_eq_inv _ _ h.unit' _

Premises used: Units.mul_eq_one_iff_eq_inv
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit a
⊢ a * b = 1 ↔ a⁻¹ = b

Tactic:
@Units.mul_eq_one_iff_inv_eq _ _ h.unit' _

Premises used: Units.mul_eq_one_iff_inv_eq
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
rw : a * b⁻¹ * b = a
rw₁ rw₂ : a = a
⊢ a / b * b = a

Tactic:
rw [div_eq_mul_inv, h.inv_mul_cancel_right]

Premises used: div_eq_mul_inv, IsUnit.inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
b : α
h : IsUnit b
a : α
rw : a * b * b⁻¹ = a
rw₁ rw₂ : a = a
⊢ a * b / b = a

Tactic:
rw [div_eq_mul_inv, h.mul_inv_cancel_right]

Premises used: IsUnit.mul_inv_cancel_right, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ a * (1 / a) = 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a : α
h : IsUnit a
⊢ 1 / a * a = 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
simp : a * c⁻¹ = b * c⁻¹ ↔ a = b
⊢ a / c = b / c ↔ a = b

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b

Tactic:
Units.mul_left_inj h.inv.unit'

Premises used: IsUnit.inv, IsUnit.unit', Units.mul_left_inj
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b

Tactic:
exact Units.mul_left_inj h.inv.unit'

Premises used: IsUnit.inv, IsUnit.unit', Units.mul_left_inj
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit b
rw : a * b⁻¹ = c ↔ a = c * b
rw₁ rw₂ : a = c * b ↔ a = c * b
⊢ a / b = c ↔ a = c * b

Tactic:
rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]

Premises used: div_eq_mul_inv, IsUnit.mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
rw : a = b * c⁻¹ ↔ a * c = b
rw₁ rw₂ : a * c = b ↔ a * c = b
⊢ a = b / c ↔ a * c = b

Tactic:
rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]

Premises used: IsUnit.eq_mul_inv_iff_mul_eq, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a = c * b → a / b = c

Tactic:
h.div_eq_iff.2

Premises used: Iff.mpr, IsUnit.div_eq_iff
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c = b → a = b / c

Tactic:
h.eq_div_iff.2

Premises used: Iff.mpr, IsUnit.eq_div_iff
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit b
⊢ a / b = 1 ↔ a = b

Tactic:
⟨eq_of_div_eq_one, fun hab => hab.symm ▸ h.div_self⟩

Premises used: IsUnit.div_self, eq_of_div_eq_one, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
a b : α
h : IsUnit b
rw : a⁻¹ = 1 / a
rw₁ rw₂ : a⁻¹ = a⁻¹
⊢ b / (a * b) = 1 / a

Tactic:
rw [h.div_mul_cancel_right, one_div]

Premises used: IsUnit.div_mul_cancel_right, one_div
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionMonoid α
b a : α
h : IsUnit b
⊢ a * b * (1 / b) = a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : a / (b * a) = 1 / b
rw₁ rw₂ : 1 / b = 1 / b
⊢ a / (a * b) = 1 / b

Tactic:
rw [mul_comm, h.div_mul_left]

Premises used: IsUnit.div_mul_left, mul_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : b * a / a = b
rw₁ rw₂ : b = b
⊢ a * b / a = b

Tactic:
rw [mul_comm, h.mul_div_cancel_right]

Premises used: mul_comm, IsUnit.mul_div_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
rw : b / a * a = b
rw₁ rw₂ : b = b
⊢ a * (b / a) = b

Tactic:
rw [mul_comm, h.div_mul_cancel]

Premises used: mul_comm, IsUnit.div_mul_cancel
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
rw₂ : a / b * b * d = c * b
rw₃ : c / d * b * d = c * b
rw₄ : c * b / d * d = c * b
rw₅ rw₆ : c * b = c * b
⊢ a * d = c * b

Tactic:
rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]

Premises used: IsUnit.div_self, div_mul_eq_mul_div, mul_comm_div, mul_one, IsUnit.div_mul_cancel
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
rw₁ : a / b * b * d = c / d * (b * d) ↔ a * d = c * b
rw₂ : a * d = c / d * (b * d) ↔ a * d = c * b
rw₃ : a * d = c / d * b * d ↔ a * d = c * b
rw₄ : a * d = c / d * d * b ↔ a * d = c * b
rw₅ rw₆ : a * d = c * b ↔ a * d = c * b
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]

Premises used: mul_assoc, IsUnit.mul, mul_right_comm, IsUnit.mul_left_inj, IsUnit.div_mul_cancel
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b = c * d⁻¹ ↔ a * d = c * b
rw₁ : a / b = c / d ↔ a * d = c * b
rw₂ rw₃ : a * d = c * b ↔ a * d = c * b
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, hb.div_eq_div_iff hd]

Premises used: div_eq_mul_inv, IsUnit.div_eq_div_iff
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
rw : a / b = d⁻¹ * c ↔ a * d = c * b
rw₁ : a / b = c / d ↔ a * d = c * b
rw₂ rw₃ : a * d = c * b ↔ a * d = c * b
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

Tactic:
rw [← div_eq_inv_mul, ← div_eq_inv_mul, hb.div_eq_div_iff hd]

Premises used: div_eq_inv_mul, IsUnit.div_eq_div_iff
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
rw : a * b / a = b
rw₁ rw₂ : b = b
⊢ a / (a / b) = b

Tactic:
rw [div_div_eq_mul_div, h.mul_div_cancel_left]

Premises used: IsUnit.mul_div_cancel_left, div_div_eq_mul_div
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : DivisionCommMonoid α
a b : α
h : IsUnit a
rw : a / b * a⁻¹ = b⁻¹
rw₁ : a * b⁻¹ * a⁻¹ = b⁻¹
rw₂ : a * a⁻¹ * b⁻¹ = b⁻¹
rw₃ : 1 * b⁻¹ = b⁻¹
rw₄ rw₅ : b⁻¹ = b⁻¹
⊢ a / b / a = b⁻¹

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]

Premises used: IsUnit.mul_inv_cancel, div_eq_mul_inv, mul_right_comm, one_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
h₁ : a * b = 1
h₂ : b * a = 1
⊢ (↑{ val := a, inv := b, val_inv := h₁, inv_val := h₂ : αˣ } : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
subst :
  ∀ (vi₂ : v * i₂ = 1) (iv₂ : i₂ * v = 1),
    { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ : αˣ } =
      { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ : αˣ } =
    { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
subst v'
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
e_inv : i₁ = i₂
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ : αˣ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂

Tactic:
simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

Premises used: mul_assoc, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u v : αˣ
huv : (↑u : α) = (↑v : α)
⊢ u = v

Tactic:
val_injective huv

Premises used: Units.val_injective
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a b : αˣ
⊢ (↑a : α) = (↑b : α) ↔ a = b

Tactic:
val_injective.eq_iff

Premises used: Function.Injective.eq_iff, Units.val_injective
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u : αˣ
y : α
h₁ : (↑u : α) * y = 1
h₂ : y * (↑u : α) = 1
⊢ { val := (↑u : α), inv := y, val_inv := h₁, inv_val := h₂ : αˣ } = u

Tactic:
ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u : αˣ
val : α
hv : val = (↑u : α)
inv : α
hi : inv = (↑u⁻¹ : α)
⊢ u.copy val hv inv hi = u

Tactic:
ext hv

Premises used: Units.ext
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
rw : (↑u₁ : α) * ((↑u₂ : α) * (u₂.inv * u₁.inv)) = 1
rw₁ : (↑u₁ : α) * ((↑u₂ : α) * u₂.inv * u₁.inv) = 1
rw₂ : (↑u₁ : α) * (1 * u₁.inv) = 1
rw₃ : (↑u₁ : α) * u₁.inv = 1
rw₄ rw₅ : Eq.{u + 1} (α := α) 1 1
⊢ (↑u₁ : α) * (↑u₂ : α) * (u₂.inv * u₁.inv) = 1

Tactic:
rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]

Premises used: Units.val, mul_assoc, Units.val_inv, one_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
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
rw₄ rw₅ : Eq.{u + 1} (α := α) 1 1
⊢ u₂.inv * u₁.inv * ((↑u₁ : α) * (↑u₂ : α)) = 1

Tactic:
rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]

Premises used: Units.inv_val, mul_assoc, Units.inv, one_mul
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a b : αˣ
⊢ (↑(a * b) : α) = (↑a : α) * (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
⊢ Eq.{u + 1} (α := α) (↑1 : α) 1

Tactic:
rfl

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

Tactic:
rw [← Units.val_one, val_inj]

Premises used: Units.val_inj, Units.val_one
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
x y : α
h₁ : x * y = 1
h₂ : y * x = 1
⊢ { val := x, inv := y, val_inv := h₁, inv_val := h₂ : αˣ }⁻¹ = { val := y, inv := x, val_inv := h₂, inv_val := h₁ }

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
inv_val _

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

Tactic:
val_inv _

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

Tactic:
rw [Commute, SemiconjBy, inv_mul, mul_inv]

Premises used: SemiconjBy, Units.inv_mul, Commute, Units.mul_inv
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : αˣ
⊢ Commute (↑a⁻¹ : α) (↑a : α)

Tactic:
a.commute_coe_inv.symm

Premises used: Units.commute_coe_inv, Commute.symm
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) = a
rw : (↑u⁻¹ : α) * (↑u : α) = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ (↑u⁻¹ : α) * a = 1

Tactic:
rw [← h, u.inv_mul]

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

Tactic:
rw [← h, u.mul_inv]

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

Tactic:
rw [← mul_assoc, mul_inv, one_mul]

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

Tactic:
rw [← mul_assoc, inv_mul, one_mul]

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

Tactic:
rw [← h, mul_inv_cancel_left]

Premises used: Units.mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a : αˣ
b c : α
h : b = (↑a : α) * c
rw : (↑a⁻¹ : α) * ((↑a : α) * c) = c
rw₁ rw₂ : c = c
⊢ (↑a⁻¹ : α) * b = c

Tactic:
rw [h, inv_mul_cancel_left]

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

Tactic:
rw [← a.commute_coe_inv.mul_pow]

Premises used: Units.commute_coe_inv, Commute.mul_pow
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
⊢ ((↑a : α) * (↑a⁻¹ : α)) ^ n = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
rw : ((↑a⁻¹ : α) * (↑a : α)) ^ n = 1
⊢ (↑a⁻¹ : α) ^ n * (↑a : α) ^ n = 1

Tactic:
rw [← a.commute_inv_coe.mul_pow]

Premises used: Units.commute_inv_coe, Commute.mul_pow
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u : αˣ
n : ℕ
a : αˣ
⊢ ((↑a⁻¹ : α) * (↑a : α)) ^ n = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b u a : αˣ
huv :
  (↑{ val := HPow.hPow (β := ℕ) (↑a : α) 0, inv := HPow.hPow (β := ℕ) (↑a⁻¹ : α) 0, val_inv := ⋯, inv_val := ⋯ : αˣ } :
      α) =
    (↑1 : α)
⊢ { val := HPow.hPow (β := ℕ) (↑a : α) 0, inv := HPow.hPow (β := ℕ) (↑a⁻¹ : α) 0, val_inv := ⋯, inv_val := ⋯ : αˣ } = 1

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

Tactic:
simp