case inl
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f (if p then 1 else 0) = 1

case inr
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f (if p then 1 else 0) = 0
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ ↑f (if p then 1 else 0) = if p then 1 else 0
split_ifs with h
case inl
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f 1 = 1
case inl
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f (if p then 1 else 0) = 1
simp only [h, ite_true]
no goals
case inl
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f 1 = 1
rw [map_one]
case inr
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f 0 = 0
case inr
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f (if p then 1 else 0) = 0
simp only [h, ite_false]
no goals
case inr
F✝ : Type ?u.83334
α : Type u_2
β : Type u_3
γ : Type ?u.83343
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_1
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f 0 = 0
rw [map_zero]