[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ ↑f ↑u * ↑f u.inv = 1
[PROOFSTEP]
rw [← f.map_mul, u.val_inv, f.map_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ ↑f u.inv * ↑f ↑u = 1
[PROOFSTEP]
rw [← f.map_mul, u.inv_val, f.map_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
⊢ map (MonoidHom.id M) = MonoidHom.id Mˣ
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : Mˣ
⊢ ↑(↑(map (MonoidHom.id M)) x✝) = ↑(↑(MonoidHom.id Mˣ) x✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a / ↑u
[PROOFSTEP]
rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ g 1 = 1
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ ↑(g 1) = ↑1
[PROOFSTEP]
dsimp only
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ ↑(g 1) = ↑1
[PROOFSTEP]
rw [h 1]
[GOAL]
case a
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
⊢ ↑f 1 = ↑1
[PROOFSTEP]
exact f.map_one
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
x y : M
⊢ ↑(OneHom.toFun { toFun := g, map_one' := (_ : g 1 = 1) } (x * y)) =
    ↑(OneHom.toFun { toFun := g, map_one' := (_ : g 1 = 1) } x *
        OneHom.toFun { toFun := g, map_one' := (_ : g 1 = 1) } y)
[PROOFSTEP]
simp only [h, val_mul, f.map_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
x : M
⊢ ↑f x * ↑(↑(liftRight f g h) x)⁻¹ = 1
[PROOFSTEP]
rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]
[GOAL]
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
x : M
⊢ ↑(↑(liftRight f g h) x)⁻¹ * ↑f x = 1
[PROOFSTEP]
rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ IsUnit (↑f x)
[PROOFSTEP]
rcases h with ⟨y, rfl⟩
[GOAL]
case intro
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit (↑f ↑y)
[PROOFSTEP]
exact (Units.map (f : M →* N) y).isUnit
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MonoidHomClass F M N
inst✝ : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse ↑g ↑f
h : IsUnit (↑f x)
⊢ IsUnit x
[PROOFSTEP]
simpa only [hfg x] using h.map g
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x : M
⊢ ∀ (x : M), ↑(IsUnit.unit (_ : IsUnit (↑f x))) = ↑f x
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x x✝ : M
⊢ ↑(IsUnit.unit (_ : IsUnit (↑f x✝))) = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x : M
⊢ ∀ (x : M), ↑(IsUnit.unit (_ : IsUnit (↑f x))) = ↑f x
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x x✝ : M
⊢ ↑(IsUnit.unit (_ : IsUnit (↑f x✝))) = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ a / a = 1
[PROOFSTEP]
rw [div_eq_mul_inv, h.mul_inv_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b c : α
h : IsUnit b
a : α
⊢ a / b * b = a
[PROOFSTEP]
rw [div_eq_mul_inv, h.inv_mul_cancel_right]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b c : α
h : IsUnit b
a : α
⊢ a * b / b = a
[PROOFSTEP]
rw [div_eq_mul_inv, h.mul_inv_cancel_right]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ a * (1 / a) = 1
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ 1 / a * a = 1
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit a
⊢ IsUnit a⁻¹
[PROOFSTEP]
rcases h with ⟨u, hu⟩
[GOAL]
case intro
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹
[PROOFSTEP]
rw [← hu, ← Units.val_inv_eq_inv_val]
[GOAL]
case intro
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹
[PROOFSTEP]
exact Units.isUnit _
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)
[PROOFSTEP]
exact ha.mul hb.inv
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b
[PROOFSTEP]
exact Units.mul_left_inj h.inv.unit'
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b
[PROOFSTEP]
rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b
[PROOFSTEP]
rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ b / (a * b) = 1 / a
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b✝ c : α
h : IsUnit c
a b : α
⊢ a * c / (b * c) = a / b
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionMonoid α
a✝ b c a : α
h : IsUnit b
⊢ a * b * (1 / b) = a
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b
[PROOFSTEP]
rw [mul_comm, h.div_mul_left]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a * b / a = b
[PROOFSTEP]
rw [mul_comm, h.mul_div_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a * (b / a) = b
[PROOFSTEP]
rw [mul_comm, h.div_mul_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a✝ b✝ c d : α
h : IsUnit c
a b : α
⊢ c * a / (c * b) = a / b
[PROOFSTEP]
rw [mul_comm c, mul_comm c, h.mul_div_mul_right]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a✝ b c✝ d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * d = c * b
[PROOFSTEP]
rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b
[PROOFSTEP]
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm, hd.div_mul_cancel]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b c d : α
h : IsUnit a
⊢ a / (a / b) = b
[PROOFSTEP]
rw [div_div_eq_mul_div, h.mul_div_cancel_left]
[GOAL]
F : Type u_1
G : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst✝ : DivisionCommMonoid α
a b c d : α
h : IsUnit a
⊢ a / b / a = b⁻¹
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]
