[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
f g : α →ₙ+* β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
g : α →ₙ+* β
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h : (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = (fun f => f.toFun) g
⊢ { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : MulHom.toFun toMulHom✝¹ 0 = 0
map_add'✝¹ : ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h :
  (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMulHom
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : MulHom.toFun toMulHom✝¹ 0 = 0
map_add'✝¹ : ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h :
  (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMulHom✝¹ = toMulHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toMulHom.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : MulHom.toFun toMulHom✝¹ 0 = 0
map_add'✝¹ : ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h :
  (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ↑toMulHom✝¹ = ↑toMulHom✝
[PROOFSTEP]
exact h
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ α →ₙ+* α
[PROOFSTEP]
refine' { toFun := id .. }
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ ∀ (x y : α), id (x * y) = id x * id y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ ∀ (x y : α),
    MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } (x + y) =
      MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } x +
        MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
x✝ y✝ : α
⊢ id (x✝ * y✝) = id x✝ * id y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
x✝ y✝ : α
⊢ MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } (x✝ + y✝) =
    MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } x✝ +
      MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } y✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g✝ : β →ₙ+* γ
f : α →ₙ+* β
g : β →ₙ+* γ
⊢ comp g 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g✝ : β →ₙ+* γ
f : α →ₙ+* β
g : β →ₙ+* γ
x✝ : α
⊢ ↑(comp g 0) x✝ = ↑0 x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f✝ f : α →ₙ+* β
⊢ comp 0 f = 0
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f✝ f : α →ₙ+* β
x✝ : α
⊢ ↑(comp 0 f) x✝ = ↑0 x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g✝ : β →ₙ+* γ
f : α →ₙ+* β
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
x : α
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonAssocSemiring α
inst✝¹ : NonAssocSemiring β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ ↑f (bit1 a) = bit1 (↑f a)
[PROOFSTEP]
simp [bit1]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f g : α →+* β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
g : α →+* β
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } =
    (fun f => f.toFun) g
⊢ { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMonoidHom
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toMonoidHom.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ↑toMonoidHom✝¹ = ↑toMonoidHom✝
[PROOFSTEP]
exact h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ ↑(toMonoidWithZeroHom f) = ↑f
[PROOFSTEP]
rfl
[GOAL]
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ ↑f (if p then 0 else 1) = if p then 0 else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f (if p then 0 else 1) = 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f (if p then 0 else 1) = 1
[PROOFSTEP]
simp [h]
[GOAL]
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ ↑f (if p then 1 else 0) = if p then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f (if p then 1 else 0) = 1
[PROOFSTEP]
simp [h]
[GOAL]
case neg
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f (if p then 1 else 0) = 0
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
x y : α
⊢ 0 = 1 ↔ ↑f 1 = 0
[PROOFSTEP]
rw [map_one, eq_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
f : α →+* β
x✝ y : α
h : ↑f 1 = 0
x : α
⊢ ↑f x = 0
[PROOFSTEP]
rw [← mul_one x, map_mul, h, mul_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝³ : NonAssocSemiring α
x✝² : NonAssocSemiring β
f : α →+* β
x✝¹ y✝ : α
h : ∀ (x : α), ↑f x = 0
y : β
x✝ : y ∈ Set.range ↑f
x : α
hx : ↑f x = y
⊢ y ∈ {0}
[PROOFSTEP]
simp [← hx, h x]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
x y✝ : α
h : ∀ (x : α), ↑f x = 0
y : β
hy : y ∈ {0}
⊢ ↑f 0 = y
[PROOFSTEP]
simpa using hy.symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
x y : α
inst✝ : Nontrivial β
h : 1 = 0
⊢ ↑f 1 = 0
[PROOFSTEP]
rw [h, map_zero]
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ α →+* α
[PROOFSTEP]
refine' { toFun := _root_.id .. }
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ _root_.id 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ ∀ (x y : α),
    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
        OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y
[PROOFSTEP]
intros
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
          map_mul' :=
            (_ :
              ∀ (x y : α),
                OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                  OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
      0 =
    0
[PROOFSTEP]
intros
[GOAL]
case refine'_4
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ ∀ (x y : α),
    OneHom.toFun
        (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
              map_mul' :=
                (_ :
                  ∀ (x y : α),
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                        OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
              map_mul' :=
                (_ :
                  ∀ (x y : α),
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                        OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
          y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ _root_.id 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α✝
x✝¹ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
x✝ y✝ : α
⊢ OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x✝ * y✝) =
    OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } x✝ *
      OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
          map_mul' :=
            (_ :
              ∀ (x y : α),
                OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
      0 =
    0
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α✝
x✝¹ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
x✝ y✝ : α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
          map_mul' :=
            (_ :
              ∀ (x y : α),
                OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
      (x✝ + y✝) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                    OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
        x✝ +
      OneHom.toFun
        (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                    OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
        y✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f : α →+* β
src✝ : α →ₙ+* γ := NonUnitalRingHom.comp (toNonUnitalRingHom g) (toNonUnitalRingHom f)
⊢ (↑g ∘ ↑f) 1 = 1
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
x : α
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
⊢ IsDomain β
[PROOFSTEP]
haveI := pullback_nonzero f f.map_zero f.map_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this : Nontrivial β
⊢ IsDomain β
[PROOFSTEP]
haveI := IsRightCancelMulZero.to_noZeroDivisors α
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝ : Nontrivial β
this : NoZeroDivisors α
⊢ IsDomain β
[PROOFSTEP]
haveI := hf.noZeroDivisors f f.map_zero f.map_mul
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝¹ : Nontrivial β
this✝ : NoZeroDivisors α
this : NoZeroDivisors β
⊢ IsDomain β
[PROOFSTEP]
exact NoZeroDivisors.to_isDomain β
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
have hxy := h (x + y)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy : ↑f ((x + y) * (x + y)) = ↑f (x + y) * ↑f (x + y)
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul, mul_add, mul_add, ←
  sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub, ← sub_sub, mul_comm y x, mul_comm (f y) (f x)] at
  hxy 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy✝ : ↑f x * ↑f x + ↑f (y * x) + (↑f (x * y) + ↑f y * ↑f y) = ↑f x * ↑f x + ↑f x * ↑f y + (↑f y * ↑f x + ↑f y * ↑f y)
hxy : ↑f (x * y) + ↑f y * ↑f y + (↑f x * ↑f x + ↑f (x * y)) - ↑f x * ↑f x - ↑f x * ↑f y - ↑f x * ↑f y - ↑f y * ↑f y = 0
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
simp only [add_assoc, add_sub_assoc, add_sub_cancel'_right] at hxy 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy✝ : ↑f x * ↑f x + ↑f (y * x) + (↑f (x * y) + ↑f y * ↑f y) = ↑f x * ↑f x + ↑f x * ↑f y + (↑f y * ↑f x + ↑f y * ↑f y)
hxy : ↑f (x * y) + (↑f (x * y) - ↑f x * ↑f y - ↑f x * ↑f y) = 0
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero (M₀ := α), sub_eq_zero,
  or_iff_not_imp_left] at hxy 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy✝ : ↑f x * ↑f x + ↑f (y * x) + (↑f (x * y) + ↑f y * ↑f y) = ↑f x * ↑f x + ↑f x * ↑f y + (↑f y * ↑f x + ↑f y * ↑f y)
hxy : ¬2 = 0 → ↑f (x * y) = ↑f x * ↑f y
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
exact hxy h_two
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
⊢ ↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) = f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x✝ : β
⊢ ↑↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) x✝ = ↑f x✝
[PROOFSTEP]
rfl
