case a
l : Type ?u.18435
m : Type u_1
n : Type u_2
o : Type ?u.18444
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = OfNat.ofNat 0 i✝ j✝
l : Type ?u.18435
m : Type u_1
n : Type u_2
o : Type ?u.18444
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
⊢ map 0 f = 0
ext
no goals
case a
l : Type ?u.18435
m : Type u_1
n : Type u_2
o : Type ?u.18444
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = OfNat.ofNat 0 i✝ j✝
simp [h]