case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
h : optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ ↑(mapRange (fun i => id) h g) i✝ = ↑g i✝
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
h : optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)
g : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i => id) h g = g
ext
no goals
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
h : optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ ↑(mapRange (fun i => id) h g) i✝ = ↑g i✝
rfl