-- Mathlib/Data/DFinsupp/Defs.lean
theorem zipWith_single_single (f : ∀ i, β₁ i → β₂ i → β i) (hf : ∀ i, f i 0 0 = 0)
    {i} (b₁ : β₁ i) (b₂ : β₂ i) :
    zipWith f hf (single i b₁) (single i b₂) = single i (f i b₁ b₂)

Proof state:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
⊢ zipWith f hf (single i b₁) (single i b₂) = single i (f i b₁ b₂)

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
j : ι
⊢ (zipWith f hf (single i b₁) (single i b₂)) j = (single i (f i b₁ b₂)) j

Proof state:
case h
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
j : ι
⊢ (zipWith f hf (single i b₁) (single i b₂)) j = (single i (f i b₁ b₂)) j

Tactic:
rw [zipWith_apply]

Result:
case h
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
j : ι
⊢ f j ((single i b₁) j) ((single i b₂) j) = (single i (f i b₁ b₂)) j

Proof state:
case h.inl
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
⊢ f i ((single i b₁) i) ((single i b₂) i) = (single i (f i b₁ b₂)) i

Tactic:
rw [single_eq_same, single_eq_same, single_eq_same]

Result:
no goals

Proof state:
case h
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
j : ι
⊢ f j ((single i b₁) j) ((single i b₂) j) = (single i (f i b₁ b₂)) j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case h.inl
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
⊢ f i ((single i b₁) i) ((single i b₂) i) = (single i (f i b₁ b₂)) i

case h.inr
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
j : ι
hij : i ≠ j
⊢ f j ((single i b₁) j) ((single i b₂) j) = (single i (f i b₁ b₂)) j

Proof state:
case h.inr
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
j : ι
hij : i ≠ j
⊢ f j ((single i b₁) j) ((single i b₂) j) = (single i (f i b₁ b₂)) j

Tactic:
rw [single_eq_of_ne hij, single_eq_of_ne hij, single_eq_of_ne hij, hf]

Result:
no goals