-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem prod_eq_prod_fintype [Fintype ι] [∀ i, Zero (β i)] [∀ (i : ι) (x : β i), Decidable (x ≠ 0)]
    -- Porting note: `f` was a typeclass argument
    [CommMonoid γ] (v : Π₀ i, β i) {f : ∀ i, β i → γ} (hf : ∀ i, f i 0 = 1) :
    v.prod f = ∏ i, f i (DFinsupp.equivFunOnFintype v i)

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ ∀ x ∈ Finset.univ, x ∉ v.support → f x (v x) = 1

Tactic:
intro i _ hi

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : i ∉ v.support
⊢ f i (v i) = 1

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : v i = 0
⊢ f i (v i) = 1

Tactic:
rw [hi, hf]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : i ∉ v.support
⊢ f i (v i) = 1

Tactic:
rw [mem_support_iff, not_not] at hi

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : v i = 0
⊢ f i (v i) = 1

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ ∏ i ∈ v.support, f i (v i) = ∏ i : ι, f i (v i)

Tactic:
apply Finset.prod_subset v.support.subset_univ

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ ∀ x ∈ Finset.univ, x ∉ v.support → f x (v x) = 1

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ v.prod f = ∏ i : ι, f i (equivFunOnFintype v i)

Tactic:
suffices (∏ i ∈ v.support, f i (v i)) = ∏ i, f i (v i) by simp [DFinsupp.prod, this]

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ ∏ i ∈ v.support, f i (v i) = ∏ i : ι, f i (v i)

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
this : ∏ i ∈ v.support, f i (v i) = ∏ i : ι, f i (v i)
⊢ v.prod f = ∏ i : ι, f i (equivFunOnFintype v i)

Tactic:
simp [DFinsupp.prod, this]

Result:
no goals