[GOAL]
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ ⅟a * (a * b) = b
[PROOFSTEP]
rw [← mul_assoc, invOf_mul_self, one_mul]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
⊢ ⅟a * (a * b) = b
[PROOFSTEP]
rw [← mul_assoc, invOf_mul_self, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ a * (⅟a * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_invOf_self, one_mul]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
⊢ a * (⅟a * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_invOf_self, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible b
⊢ a * ⅟b * b = a
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
⊢ a * ⅟b * b = a
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible b
⊢ a * b * ⅟b = a
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
⊢ a * b * ⅟b = a
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α✝ α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b
[PROOFSTEP]
apply invOf_eq_right_inv
[GOAL]
case hac
α✝ α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ a * ⅟b = 1
[PROOFSTEP]
rw [h, mul_invOf_self]
[GOAL]
α : Type u
inst✝ : Monoid α
a : α
x✝¹ x✝ : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self✝ : c * a = 1
hac : a * c = 1
⊢ { invOf := b, invOf_mul_self := hba, mul_invOf_self := hab } =
    { invOf := c, invOf_mul_self := invOf_mul_self✝, mul_invOf_self := hac }
[PROOFSTEP]
congr
[GOAL]
case e_invOf
α : Type u
inst✝ : Monoid α
a : α
x✝¹ x✝ : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self✝ : c * a = 1
hac : a * c = 1
⊢ b = c
[PROOFSTEP]
exact left_inv_eq_right_inv hba hac
[GOAL]
α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ si * s = 1
[PROOFSTEP]
rw [hs, hsi, invOf_mul_self]
[GOAL]
α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ s * si = 1
[PROOFSTEP]
rw [hs, hsi, mul_invOf_self]
[GOAL]
α : Type u
inst✝² : Ring α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b
[PROOFSTEP]
subst h
[GOAL]
α : Type u
inst✝² : Ring α
a : α
inst✝¹ inst✝ : Invertible a
⊢ ⅟a = ⅟a
[PROOFSTEP]
congr
[GOAL]
case h.e_5.h
α : Type u
inst✝² : Ring α
a : α
inst✝¹ inst✝ : Invertible a
⊢ inst✝¹ = inst✝
[PROOFSTEP]
apply Subsingleton.allEq
[GOAL]
α : Type u
inst✝¹ : Monoid α
a : α
inst✝ : Invertible a
⊢ a * ⅟a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝¹ : Monoid α
a : α
inst✝ : Invertible a
⊢ ⅟a * a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝³ : Mul α
inst✝² : One α
inst✝¹ : HasDistribNeg α
a : α
inst✝ : Invertible a
⊢ -⅟a * -a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝³ : Mul α
inst✝² : One α
inst✝¹ : HasDistribNeg α
a : α
inst✝ : Invertible a
⊢ -a * -⅟a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝³ : Monoid α
inst✝² : HasDistribNeg α
a : α
inst✝¹ : Invertible a
inst✝ : Invertible (-a)
⊢ -a * -⅟a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝¹ : Ring α
inst✝ : Invertible 2
⊢ 2 * (1 - ⅟2) = 2 * ⅟2
[PROOFSTEP]
rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel]
[GOAL]
α : Type u
inst✝¹ : NonAssocSemiring α
inst✝ : Invertible 2
⊢ ⅟2 + ⅟2 = 1
[PROOFSTEP]
rw [← two_mul, mul_invOf_self]
[GOAL]
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟b * ⅟a * (a * b) = 1
[PROOFSTEP]
simp [← mul_assoc]
[GOAL]
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ a * b * (⅟b * ⅟a) = 1
[PROOFSTEP]
simp [← mul_assoc]
[GOAL]
α : Type u
inst✝³ : Monoid α
a b : α
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a * b)
⊢ a * b * (⅟b * ⅟a) = 1
[PROOFSTEP]
simp [← mul_assoc]
[GOAL]
α : Type u
a b : α
inst✝¹ : Monoid α
c : α
inst✝ : Invertible c
h : a * c = b * c
⊢ a = b
[PROOFSTEP]
simpa using congr_arg (· * ⅟c) h
[GOAL]
α : Type u
a b : α
inst✝¹ : Monoid α
c : α
inst✝ : Invertible c
h : c * a = c * b
⊢ a = b
[PROOFSTEP]
simpa using congr_arg (⅟c * ·) h
[GOAL]
α : Type u
c a b : α
inst✝¹ : Monoid α
inst✝ : Invertible c
⊢ ⅟c * a = b ↔ a = c * b
[PROOFSTEP]
rw [← mul_left_inj_of_invertible (c := c), mul_invOf_self_assoc]
[GOAL]
α : Type u
c a b : α
inst✝¹ : Monoid α
inst✝ : Invertible c
⊢ c * a = b ↔ a = ⅟c * b
[PROOFSTEP]
rw [← mul_left_inj_of_invertible (c := ⅟c), invOf_mul_self_assoc]
[GOAL]
α : Type u
c a b : α
inst✝¹ : Monoid α
inst✝ : Invertible c
⊢ a * ⅟c = b ↔ a = b * c
[PROOFSTEP]
rw [← mul_right_inj_of_invertible (c := c), mul_invOf_mul_self_cancel]
[GOAL]
α : Type u
c a b : α
inst✝¹ : Monoid α
inst✝ : Invertible c
⊢ a * c = b ↔ a = b * ⅟c
[PROOFSTEP]
rw [← mul_right_inj_of_invertible (c := ⅟c), mul_mul_invOf_self_cancel]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ a * ⅟b = ⅟b * (b * a * ⅟b)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ ⅟b * (b * a * ⅟b) = ⅟b * (a * b * ⅟b)
[PROOFSTEP]
rw [h.eq]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ ⅟b * (a * b * ⅟b) = ⅟b * a
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * a = ⅟b * (a * b * ⅟b)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * (a * b * ⅟b) = ⅟b * (b * a * ⅟b)
[PROOFSTEP]
rw [h.eq]
[GOAL]
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * (b * a * ⅟b) = a * ⅟b
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
inst✝² : MulZeroOneClass α
a : α
inst✝¹ : Nontrivial α
inst✝ : Invertible a
ha : a = 0
⊢ 0 = ⅟a * a
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ ⅟(a * b) * a * b = 1
[PROOFSTEP]
rw [mul_assoc, invOf_mul_self]
[GOAL]
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ b * (⅟(a * b) * a) = 1
[PROOFSTEP]
rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one, one_mul]
[GOAL]
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * ⅟(a * b) * a = 1
[PROOFSTEP]
rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one, one_mul]
[GOAL]
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ a * (b * ⅟(a * b)) = 1
[PROOFSTEP]
rw [← mul_assoc, mul_invOf_self]
[GOAL]
α : Type u
inst✝² : GroupWithZero α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ b / a * (a / b) = 1
[PROOFSTEP]
simp [← mul_div_assoc]
[GOAL]
α : Type u
inst✝² : GroupWithZero α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ a / b * (b / a) = 1
[PROOFSTEP]
simp [← mul_div_assoc]
[GOAL]
α : Type u
inst✝³ : GroupWithZero α
a b : α
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a / b)
⊢ a / b * (b / a) = 1
[PROOFSTEP]
simp [← mul_div_assoc]
[GOAL]
α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a * a⁻¹ = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a⁻¹ * a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : MulOneClass R
inst✝² : MulOneClass S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ ↑f ⅟r * ↑f r = 1
[PROOFSTEP]
rw [← map_mul, invOf_mul_self, map_one]
[GOAL]
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : MulOneClass R
inst✝² : MulOneClass S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ ↑f r * ↑f ⅟r = 1
[PROOFSTEP]
rw [← map_mul, mul_invOf_self, map_one]
[GOAL]
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : MulOneClass R
inst✝² : Monoid S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
ifr : Invertible (↑f r)
h : ifr = Invertible.map f r
⊢ ↑f ⅟r = ⅟(↑f r)
[PROOFSTEP]
subst h
[GOAL]
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : MulOneClass R
inst✝² : Monoid S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ ↑f ⅟r = ⅟(↑f r)
[PROOFSTEP]
rfl