case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b ≠ 0
⊢ prod (single i b) h✝ = h✝ i b

case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : ¬b ≠ 0
⊢ prod (single i b) h✝ = h✝ i b
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h : (i : ι) → β i → γ
h_zero : h i 0 = 1
⊢ prod (single i b) h = h i b
by_cases h : b ≠ 0
no goals
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b ≠ 0
⊢ prod (single i b) h✝ = h✝ i b
simp [Dfinsupp.prod, support_single_ne_zero h]
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod (single i b) h✝ = h✝ i b
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : ¬b ≠ 0
⊢ prod (single i b) h✝ = h✝ i b
rw [not_not] at h
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod 0 h✝ = 1
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod (single i b) h✝ = h✝ i b
simp [h, prod_zero_index, h_zero]
no goals
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod 0 h✝ = 1
rfl