[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
r : R
neZero : NeZero (↑f r)
h : r = 0
⊢ ↑f r = 0
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
r : R
neZero : NeZero (↑f r)
h : r = 0
⊢ ↑f 0 = 0
[PROOFSTEP]
exact ZeroHomClass.map_zero f
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝³ : Zero R
r : R
inst✝² : NeZero r
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
hf : Function.Injective ↑f
⊢ ↑f r ≠ 0
[PROOFSTEP]
rw [← ZeroHomClass.map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
R : Type u_9
M : Type u_10
inst✝³ : Zero R
r : R
inst✝² : NeZero r
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
hf : Function.Injective ↑f
⊢ ↑f r ≠ ↑f 0
[PROOFSTEP]
exact hf.ne NeZero.out
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : One M
inst✝ : One N
f g : OneHom M N
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : One M
inst✝ : One N
g : OneHom M N
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝, map_one' := map_one'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_one' := map_one'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : One M
inst✝ : One N
toFun✝¹ : M → N
map_one'✝¹ : toFun✝¹ 1 = 1
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun = { toFun := toFun✝, map_one' := map_one'✝ }.toFun
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹ } = { toFun := toFun✝, map_one' := map_one'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : Mul N
f g : M →ₙ* N
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : Mul N
g : M →ₙ* N
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : Mul N
toFun✝¹ : M → N
map_mul'✝¹ : ∀ (x y : M), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun = { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } = { toFun := toFun✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f g : M →* N
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
g : M →* N
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h : (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = (fun f => f.toFun) g
⊢ { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h :
  (fun f => f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } = { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toOneHom
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h :
  (fun f => f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ toOneHom✝¹ = toOneHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toOneHom.a
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), OneHom.toFun toOneHom✝¹ (x * y) = OneHom.toFun toOneHom✝¹ x * OneHom.toFun toOneHom✝¹ y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), OneHom.toFun toOneHom✝ (x * y) = OneHom.toFun toOneHom✝ x * OneHom.toFun toOneHom✝ y
h :
  (fun f => f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ ↑toOneHom✝¹ = ↑toOneHom✝
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ ↑f a * ↑f b = 1
[PROOFSTEP]
rw [← map_mul, h, map_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (a : G), ↑f a⁻¹ = (↑f a)⁻¹
a b : G
⊢ ↑f (a / b) = ↑f a / ↑f b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ ↑f (a * b⁻¹) = ↑f a * (↑f b)⁻¹
[PROOFSTEP]
rw [map_mul, map_inv]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
⊢ ↑f (a ^ 0) = ↑f a ^ 0
[PROOFSTEP]
rw [pow_zero, pow_zero, map_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ ↑f (a ^ (n + 1)) = ↑f a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, pow_succ, map_mul, map_pow f a n]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), ↑f x⁻¹ = (↑f x)⁻¹
a : G
n : ℕ
⊢ ↑f (a ^ ↑n) = ↑f a ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, map_pow, zpow_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), ↑f x⁻¹ = (↑f x)⁻¹
a : G
n : ℕ
⊢ ↑f (a ^ Int.negSucc n) = ↑f a ^ Int.negSucc n
[PROOFSTEP]
rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc, ← zpow_negSucc]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
f g : M →*₀ N
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
g : M →*₀ N
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h : (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = (fun f => f.toFun) g
⊢ { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
toZeroHom✝¹ : ZeroHom M N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toZeroHom
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
toZeroHom✝¹ : ZeroHom M N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ toZeroHom✝¹ = toZeroHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toZeroHom.a
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
toZeroHom✝¹ : ZeroHom M N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom M N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ ↑toZeroHom✝¹ = ↑toZeroHom✝
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
hnp : OneHom N P
hmn : OneHom M N
⊢ (↑hnp ∘ ↑hmn) 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
hnp : N →ₙ* P
hmn : M →ₙ* N
x y : M
⊢ (↑hnp ∘ ↑hmn) (x * y) = (↑hnp ∘ ↑hmn) x * (↑hnp ∘ ↑hmn) y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
hnp : N →* P
hmn : M →* N
⊢ (↑hnp ∘ ↑hmn) 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
hnp : N →* P
hmn : M →* N
⊢ ∀ (x y : M),
    OneHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) } (x * y) =
      OneHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) } x *
        OneHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_one' := (_ : ↑hnp (↑hmn 1) = 1) } y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
hnp : N →*₀ P
hmn : M →*₀ N
⊢ (↑hnp ∘ ↑hmn) 0 = 0
[PROOFSTEP]
rw [Function.comp_apply, map_zero, map_zero]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
hnp : N →*₀ P
hmn : M →*₀ N
⊢ ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
hnp : N →*₀ P
hmn : M →*₀ N
⊢ ∀ (x y : M),
    ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } (x * y) =
      ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } x *
        ZeroHom.toFun { toFun := ↑hnp ∘ ↑hmn, map_zero' := (_ : (↑hnp ∘ ↑hmn) 0 = 0) } y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← OneHom.comp_apply, h, OneHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← MulHom.comp_apply, h, MulHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f₁ f₂ : M →* N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
g : N →*₀ P
f₁ f₂ : M →*₀ N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← MonoidWithZeroHom.comp_apply, h, MonoidWithZeroHom.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
⊢ comp f 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
[PROOFSTEP]
simp only [OneHom.map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ (fun m => ↑f m * ↑g m) (x * y) = (fun m => ↑f m * ↑g m) x * (fun m => ↑f m * ↑g m) y
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ (fun m => ↑f m * ↑g m) (x * y) = (fun m => ↑f m * ↑g m) x * (fun m => ↑f m * ↑g m) y
[PROOFSTEP]
show f (x * y) * g (x * y) = f x * g x * (f y * g y)
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ ↑f (x * y) * ↑g (x * y) = ↑f x * ↑g x * (↑f y * ↑g y)
[PROOFSTEP]
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ comp g (f₁ * f₂) = comp g f₁ * comp g f₂
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ ↑(comp g (f₁ * f₂)) x✝ = ↑(comp g f₁ * comp g f₂) x✝
[PROOFSTEP]
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
⊢ ↑f 1 * ↑g 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } x *
      OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } y
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } (x * y) =
    OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } x *
      OneHom.toFun { toFun := fun m => ↑f m * ↑g m, map_one' := (_ : ↑f 1 * ↑g 1 = 1) } y
[PROOFSTEP]
show f (x * y) * g (x * y) = f x * g x * (f y * g y)
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
M : Type ?u.198672
N : Type ?u.198675
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ ↑f (x * y) * ↑g (x * y) = ↑f x * ↑g x * (↑f y * ↑g y)
[PROOFSTEP]
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ comp f 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ ↑(comp f 1) x✝ = ↑1 x✝
[PROOFSTEP]
simp only [map_one, coe_comp, Function.comp_apply, one_apply]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ comp g (f₁ * f₂) = comp g f₁ * comp g f₂
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G
inst✝³ : CommGroup H
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
x✝ : M
⊢ ↑(comp g (f₁ * f₂)) x✝ = ↑(comp g f₁ * comp g f₂) x✝
[PROOFSTEP]
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H
inst✝¹ : Group α
inst✝ : DivisionMonoid β
f : α →* β
g h : α
⊢ ↑f (g * h⁻¹) = ↑f g * (↑f h)⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G✝ : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝⁴ : Group G✝
inst✝³ : CommGroup H✝
G : Type u_9
H : Type u_10
inst✝² : Group G
inst✝¹ : MulOneClass H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), ↑f a = 1 → a = 1
x y : G
hxy : ↑f x = ↑f y
⊢ ↑f (x * y⁻¹) = 1
[PROOFSTEP]
rw [map_mul, hxy, ← map_mul, mul_inv_self, map_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝² : Group G
inst✝¹ : CommGroup H
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 * ?m.224335 f map_mul = ?m.224335 f map_mul
[PROOFSTEP]
rw [← map_mul, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f (x * y) = f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹
[PROOFSTEP]
{simp only [one_mul, inv_one, ← map_div, inv_inv]
}
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f (x * y) = f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹
[PROOFSTEP]
simp only [one_mul, inv_one, ← map_div, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y
[PROOFSTEP]
{ simp only [map_div]
  simp only [mul_right_inv, one_mul, inv_inv]
}
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y
[PROOFSTEP]
simp only [map_div]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y
[PROOFSTEP]
simp only [mul_right_inv, one_mul, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H✝ : Type u_7
F : Type u_8
inst✝³ : Group G
inst✝² : CommGroup H✝
inst✝¹ : MulOneClass M
H : Type u_9
inst✝ : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G✝ : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G✝
inst✝³ : CommGroup H
inst✝² : MulOneClass M✝
M : Type ?u.229390
G : Type ?u.229393
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
f : M →* G
a b : M
⊢ (↑f (a * b))⁻¹ = (↑f a)⁻¹ * (↑f b)⁻¹
[PROOFSTEP]
rw [← mul_inv, f.map_mul]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
N : Type u_10
A : Type u_11
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommGroup A
φ : N →* A
ψ : M →* N
⊢ comp φ⁻¹ ψ = (comp φ ψ)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
N : Type u_10
A : Type u_11
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommGroup A
φ : N →* A
ψ : M →* N
x✝ : M
⊢ ↑(comp φ⁻¹ ψ) x✝ = ↑(comp φ ψ)⁻¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, inv_apply, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
A : Type u_10
B : Type u_11
inst✝² : MulOneClass M
inst✝¹ : CommGroup A
inst✝ : CommGroup B
φ : A →* B
ψ : M →* A
⊢ comp φ ψ⁻¹ = (comp φ ψ)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_9
A : Type u_10
B : Type u_11
inst✝² : MulOneClass M
inst✝¹ : CommGroup A
inst✝ : CommGroup B
φ : A →* B
ψ : M →* A
x✝ : M
⊢ ↑(comp φ ψ⁻¹) x✝ = ↑(comp φ ψ)⁻¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, inv_apply, map_inv, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
M✝ : Type u_3
N : Type u_4
P : Type u_5
G✝ : Type u_6
H : Type u_7
F : Type u_8
inst✝⁴ : Group G✝
inst✝³ : CommGroup H
inst✝² : MulOneClass M✝
M : Type ?u.233732
G : Type ?u.233735
inst✝¹ : MulOneClass M
inst✝ : CommGroup G
f g : M →* G
a b : M
⊢ ↑f (a * b) / ↑g (a * b) = ↑f a / ↑g a * (↑f b / ↑g b)
[PROOFSTEP]
simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : CommMonoidWithZero N
f g : M →*₀ N
src✝ : M →* N := ↑f * ↑g
⊢ (fun a => ↑f a * ↑g a) 0 = 0
[PROOFSTEP]
dsimp only []
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
G : Type u_6
H : Type u_7
F : Type u_8
inst✝¹ : MulZeroOneClass M
inst✝ : CommMonoidWithZero N
f g : M →*₀ N
src✝ : M →* N := ↑f * ↑g
⊢ ↑f 0 * ↑g 0 = 0
[PROOFSTEP]
rw [map_zero, zero_mul]
