case a.h
l : Type ?u.76780
m : Type ?u.76783
n : Type u_1
o : Type ?u.76789
m' : o → Type ?u.76794
n' : o → Type ?u.76799
R : Type ?u.76802
S : Type ?u.76805
α : Type v
β : Type w
γ : Type ?u.76812
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
⊢ map 1 f i✝ x✝ = OfNat.ofNat 1 i✝ x✝
l : Type ?u.76780
m : Type ?u.76783
n : Type u_1
o : Type ?u.76789
m' : o → Type ?u.76794
n' : o → Type ?u.76799
R : Type ?u.76802
S : Type ?u.76805
α : Type v
β : Type w
γ : Type ?u.76812
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
⊢ map 1 f = 1
ext
case a.h
l : Type ?u.76780
m : Type ?u.76783
n : Type u_1
o : Type ?u.76789
m' : o → Type ?u.76794
n' : o → Type ?u.76799
R : Type ?u.76802
S : Type ?u.76805
α : Type v
β : Type w
γ : Type ?u.76812
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
⊢ f (if i✝ = x✝ then 1 else 0) = if i✝ = x✝ then 1 else 0
case a.h
l : Type ?u.76780
m : Type ?u.76783
n : Type u_1
o : Type ?u.76789
m' : o → Type ?u.76794
n' : o → Type ?u.76799
R : Type ?u.76802
S : Type ?u.76805
α : Type v
β : Type w
γ : Type ?u.76812
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
⊢ map 1 f i✝ x✝ = OfNat.ofNat 1 i✝ x✝
simp only [one_apply, map_apply]
no goals
case a.h
l : Type ?u.76780
m : Type ?u.76783
n : Type u_1
o : Type ?u.76789
m' : o → Type ?u.76794
n' : o → Type ?u.76799
R : Type ?u.76802
S : Type ?u.76805
α : Type v
β : Type w
γ : Type ?u.76812
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ x✝ : n
⊢ f (if i✝ = x✝ then 1 else 0) = if i✝ = x✝ then 1 else 0
split_ifs <;> simp [h₀, h₁]