case top
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (↑f) (⊤ + b) = map ↑f ⊤ + map (↑f) b

case coe
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (↑f) (↑a✝ + b) = map ↑f ↑a✝ + map (↑f) b
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a b : WithTop α
⊢ map (↑f) (a + b) = map (↑f) a + map (↑f) b
induction a using WithTop.recTopCoe
no goals
case top
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (↑f) (⊤ + b) = map ↑f ⊤ + map (↑f) b
exact (top_add _).symm
case coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (↑f) (↑a✝ + ⊤) = map ↑f ↑a✝ + map ↑f ⊤

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (↑f) (↑a✝¹ + ↑a✝) = map ↑f ↑a✝¹ + map ↑f ↑a✝
case coe
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (↑f) (↑a✝ + b) = map ↑f ↑a✝ + map (↑f) b
induction b using WithTop.recTopCoe
no goals
case coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (↑f) (↑a✝ + ⊤) = map ↑f ↑a✝ + map ↑f ⊤
exact (add_top _).symm
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ↑f ↑(a✝¹ + a✝) = ↑(↑f (a✝¹ + a✝))
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (↑f) (↑a✝¹ + ↑a✝) = map ↑f ↑a✝¹ + map ↑f ↑a✝
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
no goals
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ↑f ↑(a✝¹ + a✝) = ↑(↑f (a✝¹ + a✝))
rfl