no goals
α : Type ?u.10603
β : Type ?u.10606
γ : Type ?u.10609
ι : Type ?u.10612
M : Type ?u.10615
M' : Type ?u.10618
N : Type ?u.10621
P : Type ?u.10624
G : Type ?u.10627
H : Type ?u.10630
R : Type ?u.10633
S : Type ?u.10636
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M ≃ N
hf : ↑f 0 = 0
hf' : ↑f.symm 0 = 0
f₂ : N ≃ P
hf₂ : ↑f₂ 0 = 0
hf₂' : ↑f₂.symm 0 = 0
⊢ ↑(f.trans f₂) 0 = 0
rw [Equiv.trans_apply, hf, hf₂]
no goals
α : Type ?u.10603
β : Type ?u.10606
γ : Type ?u.10609
ι : Type ?u.10612
M : Type ?u.10615
M' : Type ?u.10618
N : Type ?u.10621
P : Type ?u.10624
G : Type ?u.10627
H : Type ?u.10630
R : Type ?u.10633
S : Type ?u.10636
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M ≃ N
hf : ↑f 0 = 0
hf' : ↑f.symm 0 = 0
f₂ : N ≃ P
hf₂ : ↑f₂ 0 = 0
hf₂' : ↑f₂.symm 0 = 0
⊢ ↑(f.trans f₂).symm 0 = 0
rw [Equiv.symm_trans_apply, hf₂', hf']