[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 : ↑{ 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₂ }
[PROOFSTEP]
simp only at e 
[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'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
[PROOFSTEP]
subst v'
[GOAL]
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
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₂ }
[PROOFSTEP]
congr
[GOAL]
case e_inv
α : 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₂
[PROOFSTEP]
simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁
[GOAL]
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * ↑u₂ * (u₂.inv * u₁.inv) = 1
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * u₁.inv * (↑u₁ * ↑u₂) = 1
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u a : αˣ
⊢ ↑a = 1 ↔ a = 1
[PROOFSTEP]
rw [← Units.val_one, eq_iff]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u = a
⊢ ↑u⁻¹ * a = 1
[PROOFSTEP]
rw [← h, u.inv_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u = a
⊢ a * ↑u⁻¹ = 1
[PROOFSTEP]
rw [← h, u.mul_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u a : αˣ
b : α
⊢ ↑a * (↑a⁻¹ * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_inv, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u a : αˣ
b : α
⊢ ↑a⁻¹ * (↑a * b) = b
[PROOFSTEP]
rw [← mul_assoc, inv_mul, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a : α
b : αˣ
⊢ a * ↑b * ↑b⁻¹ = a
[PROOFSTEP]
rw [mul_assoc, mul_inv, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a : α
b : αˣ
⊢ a * ↑b⁻¹ * ↑b = a
[PROOFSTEP]
rw [mul_assoc, inv_mul, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c✝ u a : αˣ
b c : α
h : ↑a * b = ↑a * c
⊢ b = c
[PROOFSTEP]
simpa only [inv_mul_cancel_left] using congr_arg (fun x : α => ↑(a⁻¹ : αˣ) * x) h
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c✝ u a : αˣ
b c : α
h : b * ↑a = c * ↑a
⊢ b = c
[PROOFSTEP]
simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a b : α
h : a = b * ↑c⁻¹
⊢ a * ↑c = b
[PROOFSTEP]
rw [h, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b✝ c u : αˣ
a b : α
h : a * ↑c = b
⊢ a = b * ↑c⁻¹
[PROOFSTEP]
rw [← h, mul_inv_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : a = ↑b⁻¹ * c
⊢ ↑b * a = c
[PROOFSTEP]
rw [h, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : ↑b * a = c
⊢ a = ↑b⁻¹ * c
[PROOFSTEP]
rw [← h, inv_mul_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a b✝ c✝ u : αˣ
b c : α
h : ↑a⁻¹ * b = c
⊢ b = ↑a * c
[PROOFSTEP]
rw [← h, mul_inv_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a b✝ c✝ u : αˣ
b c : α
h : b = ↑a * c
⊢ ↑a⁻¹ * b = c
[PROOFSTEP]
rw [h, inv_mul_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : a * ↑b⁻¹ = c
⊢ a = c * ↑b
[PROOFSTEP]
rw [← h, inv_mul_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : a = c * ↑b
⊢ a * ↑b⁻¹ = c
[PROOFSTEP]
rw [h, mul_inv_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : a * ↑u = 1
⊢ ↑u⁻¹ = 1 * ↑u⁻¹
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : a * ↑u = 1
⊢ 1 * ↑u⁻¹ = a
[PROOFSTEP]
rw [← h, mul_inv_cancel_right]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ = ↑u⁻¹ * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ * 1 = a
[PROOFSTEP]
rw [← h, inv_mul_cancel_left]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
⊢ a * ↑u = 1 ↔ a = ↑u⁻¹
[PROOFSTEP]
rw [← mul_inv_eq_one, inv_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c u : αˣ
a : α
⊢ ↑u * a = 1 ↔ ↑u⁻¹ = a
[PROOFSTEP]
rw [← inv_mul_eq_one, inv_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c u u₁ u₂ : αˣ
h : ↑u₁ = ↑u₂
⊢ ↑u₁ * ↑u₂⁻¹ = 1
[PROOFSTEP]
rw [h, u₂.mul_inv]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c a : α
u : αˣ
⊢ a * (↑u⁻¹ * ↑u) = a
[PROOFSTEP]
rw [Units.inv_mul, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c a : α
u : αˣ
⊢ a * (↑u * ↑u⁻¹) = a
[PROOFSTEP]
rw [Units.mul_inv, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u₁ u₂ : αˣ
⊢ x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
[PROOFSTEP]
simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u : αˣ
y : α
⊢ x /ₚ u * ↑u = y * ↑u ↔ y * ↑u = x
[PROOFSTEP]
rw [divp_mul_cancel]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u : αˣ
y : α
⊢ x = y * ↑u ↔ y * ↑u = x
[PROOFSTEP]
exact ⟨Eq.symm, Eq.symm⟩
[GOAL]
α : Type u
inst✝ : Monoid α
a b c x : α
u : αˣ
y : α
⊢ x = y /ₚ u ↔ x * ↑u = y
[PROOFSTEP]
rw [eq_comm, divp_eq_iff_mul_eq]
[GOAL]
α : Type u
inst✝ : Monoid α
a✝ b c a : α
u : αˣ
⊢ a /ₚ u * ↑u = 1 * ↑u ↔ a = ↑u
[PROOFSTEP]
rw [divp_mul_cancel, one_mul]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c : α
u : αˣ
⊢ ↑u⁻¹ = 1 /ₚ u
[PROOFSTEP]
rw [one_divp]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c : α
u : αˣ
⊢ ↑(1 / u) = 1 /ₚ u
[PROOFSTEP]
rw [one_div, one_divp]
[GOAL]
α : Type u
inst✝ : Monoid α
a b c : α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ /ₚ u₂
[PROOFSTEP]
rw [divp, division_def, Units.val_mul]
[GOAL]
α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x /ₚ u * y = x * y /ₚ u
[PROOFSTEP]
rw [divp, divp, mul_right_comm]
[GOAL]
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux
[PROOFSTEP]
rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
[GOAL]
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
[PROOFSTEP]
rw [divp_mul_eq_mul_divp, divp_assoc', divp_divp_eq_divp_mul]
[GOAL]
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1
[PROOFSTEP]
exact mul_one _
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, a * b = 1
[PROOFSTEP]
rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩
[GOAL]
case intro.mk
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1
[PROOFSTEP]
exact ⟨b, hab⟩
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, b * a = 1
[PROOFSTEP]
rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩
[GOAL]
case intro.mk
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b : M
val_inv✝ : a * b = 1
hba : b * a = 1
⊢ ∃ b_1, b_1 * ↑{ val := a, inv := b, val_inv := val_inv✝, inv_val := hba } = 1
[PROOFSTEP]
exact ⟨b, hba⟩
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : CommMonoid M
a : M
⊢ IsUnit a ↔ ∃ b, b * a = 1
[PROOFSTEP]
simp [isUnit_iff_exists_inv, mul_comm]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
x y : M
⊢ IsUnit x → IsUnit y → IsUnit (x * y)
[PROOFSTEP]
rintro ⟨x, rfl⟩ ⟨y, rfl⟩
[GOAL]
case intro.intro
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
x y : Mˣ
⊢ IsUnit (↑x * ↑y)
[PROOFSTEP]
exact ⟨x * y, Units.val_mul _ _⟩
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit a
[PROOFSTEP]
have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit (a * ↑u * ↑u⁻¹)
[PROOFSTEP]
exists v * u⁻¹
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ ↑(v * u⁻¹) = a * ↑u * ↑u⁻¹
[PROOFSTEP]
rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * ↑u * ↑u⁻¹)
⊢ IsUnit a
[PROOFSTEP]
rwa [mul_assoc, Units.mul_inv, mul_one] at this 
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit a
[PROOFSTEP]
have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit (↑u⁻¹ * (↑u * a))
[PROOFSTEP]
exists u⁻¹ * v
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ ↑(u⁻¹ * v) = ↑u⁻¹ * (↑u * a)
[PROOFSTEP]
rw [← hv, Units.val_mul]
[GOAL]
α : Type u
M✝ : Type u_1
N : Type u_2
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit (↑u⁻¹ * (↑u * a))
⊢ IsUnit a
[PROOFSTEP]
rwa [← mul_assoc, Units.inv_mul, one_mul] at this 
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : CommMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * (y * z) = 1
[PROOFSTEP]
rwa [← mul_assoc]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : CommMonoid M
x y : M
hu : IsUnit (x * y)
⊢ IsUnit (y * x)
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b c : M
h : IsUnit a
⊢ a * ↑(IsUnit.unit h)⁻¹ = 1
[PROOFSTEP]
rw [← h.unit.mul_inv]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : Monoid M
a b c : M
h : IsUnit a
⊢ a * ↑(IsUnit.unit h)⁻¹ = ↑(IsUnit.unit h) * ↑(IsUnit.unit h)⁻¹
[PROOFSTEP]
congr
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
a : M
⊢ IsUnit a → a⁻¹ * a = 1
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case intro
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
u : Mˣ
⊢ (↑u)⁻¹ * ↑u = 1
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val, Units.inv_mul]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
a : M
⊢ IsUnit a → a * a⁻¹ = 1
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case intro
α : Type u
M : Type u_1
N : Type u_2
inst✝ : DivisionMonoid M
u : Mˣ
⊢ ↑u * (↑u)⁻¹ = 1
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val, Units.mul_inv]
[GOAL]
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1
[PROOFSTEP]
change ↑(h a).unit⁻¹ * a = 1
[GOAL]
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑(IsUnit.unit (_ : IsUnit a))⁻¹ * a = 1
[PROOFSTEP]
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
[GOAL]
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1
[PROOFSTEP]
change ↑(h a).unit⁻¹ * a = 1
[GOAL]
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑(IsUnit.unit (_ : IsUnit a))⁻¹ * a = 1
[PROOFSTEP]
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
