[GOAL]
G : Type u_1
M : Type u
⊢ ∀ ⦃m₁ m₂ : MulOneClass M⦄, Mul.mul = Mul.mul → m₁ = m₂
[PROOFSTEP]
rintro @⟨⟨one₁⟩, ⟨mul₁⟩, one_mul₁, mul_one₁⟩ @⟨⟨one₂⟩, ⟨mul₂⟩, one_mul₂, mul_one₂⟩
  ⟨rfl⟩
      -- FIXME (See https://github.com/leanprover/lean4/issues/1711)
        -- congr
[GOAL]
case mk.mk.mk.mk.mk.mk.refl
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂
[PROOFSTEP]
suffices one₁ = one₂ by cases this; rfl
[GOAL]
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
this : one₁ = one₂
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂
[PROOFSTEP]
cases this
[GOAL]
case refl
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.mk.mk.mk.mk.refl
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ one₁ = one₂
[PROOFSTEP]
exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)
[GOAL]
G : Type u_1
M : Type u
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c
[PROOFSTEP]
rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
[GOAL]
G : Type u_1
inst✝ : DivInvMonoid G
a✝ b a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
[PROOFSTEP]
rw [← zpow_ofNat]
[GOAL]
G : Type u_1
inst✝ : DivInvMonoid G
a✝ b a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹
[PROOFSTEP]
exact DivInvMonoid.zpow_neg' n a
[GOAL]
G✝ : Type u_1
inst✝¹ : DivInvMonoid G✝
a✝ b : G✝
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)
[PROOFSTEP]
rw [← ofNat_zsmul]
[GOAL]
G✝ : Type u_1
inst✝¹ : DivInvMonoid G✝
a✝ b : G✝
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)
[PROOFSTEP]
exact SubNegMonoid.zsmul_neg' n a
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b c a : G
⊢ a * a⁻¹ = 1
[PROOFSTEP]
rw [← mul_left_inv a⁻¹, inv_eq_of_mul (mul_left_inv a)]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a⁻¹ * (a * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_left_inv, one_mul]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * (a⁻¹ * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_right_inv, one_mul]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * b * b⁻¹ = a
[PROOFSTEP]
rw [mul_assoc, mul_right_inv, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * b⁻¹ * b = a
[PROOFSTEP]
rw [mul_assoc, mul_left_inv, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * b * (b⁻¹ * a⁻¹) = 1
[PROOFSTEP]
rw [mul_assoc, mul_inv_cancel_left, mul_right_inv]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c✝ : G
src✝ : Group G := inst✝
a b c : G
h : a * b = a * c
⊢ b = c
[PROOFSTEP]
rw [← inv_mul_cancel_left a b, h, inv_mul_cancel_left]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c✝ : G
src✝ : Group G := inst✝
a b c : G
h : a * b = c * b
⊢ a = c
[PROOFSTEP]
rw [← mul_inv_cancel_right a b, h, mul_inv_cancel_right]
[GOAL]
G✝ : Type u_1
G : Type u_2
⊢ Injective (@toDivInvMonoid G)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.refl
G✝ : Type u_1
G : Type u_2
toDivInvMonoid✝ : DivInvMonoid G
mul_left_inv✝¹ mul_left_inv✝ : ∀ (a : G), a⁻¹ * a = 1
⊢ mk mul_left_inv✝¹ = mk mul_left_inv✝
[PROOFSTEP]
rfl
[GOAL]
G✝ : Type u_1
G : Type u
⊢ Injective (@toGroup G)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.refl
G✝ : Type u_1
G : Type u
toGroup✝ : Group G
mul_comm✝¹ mul_comm✝ : ∀ (a b : G), a * b = b * a
⊢ mk mul_comm✝¹ = mk mul_comm✝
[PROOFSTEP]
rfl
