no goals
R : Type ?u.17787
α : Type u_1
α' : Type ?u.17793
β : Type u_2
β' : Type ?u.17799
γ : Type u_3
γ' : Type ?u.17805
l : Type ?u.17808
m : Type u_4
n : Type u_5
p : Type ?u.17817
q : Type ?u.17820
r : Type ?u.17823
l' : Type ?u.17826
m' : Type ?u.17829
n' : Type ?u.17832
p' : Type ?u.17835
inst✝⁷ : Zero α
inst✝⁶ : Zero β
inst✝⁵ : Zero γ
inst✝⁴ : One α
inst✝³ : One β
inst✝² : One γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
hf₃ : f 1 1 = 1
⊢ (diagonal fun mn => f 1 1) = 1
simp only [hf₃, diagonal_one]