case h
ι✝ : Type u
γ : Type w
β✝ : ι✝ → Type v
β₁✝ : ι✝ → Type v₁
β₂✝ : ι✝ → Type v₂
dec✝ : DecidableEq ι✝
inst✝¹⁰ : (i : ι✝) → Zero (β✝ i)
inst✝⁹ : (i : ι✝) → (x : β✝ i) → Decidable (x ≠ 0)
inst✝⁸ : (i : ι✝) → Zero (β₁✝ i)
inst✝⁷ : (i : ι✝) → Zero (β₂✝ i)
inst✝⁶ : (i : ι✝) → (x : β₁✝ i) → Decidable (x ≠ 0)
inst✝⁵ : (i : ι✝) → (x : β₂✝ i) → Decidable (x ≠ 0)
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
i : ι
⊢ ↑(zipWith f hf g₁ g₂) i = ↑(mk (support g₁ ∪ support g₂) fun i => f (↑i) (↑g₁ ↑i) (↑g₂ ↑i)) i
ι✝ : Type u
γ : Type w
β✝ : ι✝ → Type v
β₁✝ : ι✝ → Type v₁
β₂✝ : ι✝ → Type v₂
dec✝ : DecidableEq ι✝
inst✝¹⁰ : (i : ι✝) → Zero (β✝ i)
inst✝⁹ : (i : ι✝) → (x : β✝ i) → Decidable (x ≠ 0)
inst✝⁸ : (i : ι✝) → Zero (β₁✝ i)
inst✝⁷ : (i : ι✝) → Zero (β₂✝ i)
inst✝⁶ : (i : ι✝) → (x : β₁✝ i) → Decidable (x ≠ 0)
inst✝⁵ : (i : ι✝) → (x : β₂✝ i) → Decidable (x ≠ 0)
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
⊢ zipWith f hf g₁ g₂ = mk (support g₁ ∪ support g₂) fun i => f (↑i) (↑g₁ ↑i) (↑g₂ ↑i)
ext i
no goals
case h
ι✝ : Type u
γ : Type w
β✝ : ι✝ → Type v
β₁✝ : ι✝ → Type v₁
β₂✝ : ι✝ → Type v₂
dec✝ : DecidableEq ι✝
inst✝¹⁰ : (i : ι✝) → Zero (β✝ i)
inst✝⁹ : (i : ι✝) → (x : β✝ i) → Decidable (x ≠ 0)
inst✝⁸ : (i : ι✝) → Zero (β₁✝ i)
inst✝⁷ : (i : ι✝) → Zero (β₂✝ i)
inst✝⁶ : (i : ι✝) → (x : β₁✝ i) → Decidable (x ≠ 0)
inst✝⁵ : (i : ι✝) → (x : β₂✝ i) → Decidable (x ≠ 0)
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
i : ι
⊢ ↑(zipWith f hf g₁ g₂) i = ↑(mk (support g₁ ∪ support g₂) fun i => f (↑i) (↑g₁ ↑i) (↑g₂ ↑i)) i
by_cases h1 : g₁ i ≠ 0 <;> by_cases h2 : g₂ i ≠ 0 <;> simp only [not_not, Ne.def] at h1 h2 <;>
  simp [h1, h2, hf]