case h
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ↑(factorization (Finset.prod S g)) p = ↑(∑ x in S, factorization (g x)) p
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
⊢ factorization (Finset.prod S g) = ∑ x in S, factorization (g x)
ext p
case h.refine'_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ↑(factorization (Finset.prod ∅ g)) p = ↑(∑ x in ∅, factorization (g x)) p

case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ∀ {a : α} {s : Finset α},
    a ∈ S →
      s ⊆ S →
        ¬a ∈ s →
          ↑(factorization (Finset.prod s g)) p = ↑(∑ x in s, factorization (g x)) p →
            ↑(factorization (Finset.prod (insert a s) g)) p = ↑(∑ x in insert a s, factorization (g x)) p
case h
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ↑(factorization (Finset.prod S g)) p = ↑(∑ x in S, factorization (g x)) p
refine' Finset.induction_on' S ?_ ?_
no goals
case h.refine'_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ↑(factorization (Finset.prod ∅ g)) p = ↑(∑ x in ∅, factorization (g x)) p
simp
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : ¬x ∈ T
IH : ↑(factorization (Finset.prod T g)) p = ↑(∑ x in T, factorization (g x)) p
⊢ ↑(factorization (Finset.prod (insert x T) g)) p = ↑(∑ x in insert x T, factorization (g x)) p
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ∀ {a : α} {s : Finset α},
    a ∈ S →
      s ⊆ S →
        ¬a ∈ s →
          ↑(factorization (Finset.prod s g)) p = ↑(∑ x in s, factorization (g x)) p →
            ↑(factorization (Finset.prod (insert a s) g)) p = ↑(∑ x in insert a s, factorization (g x)) p
intro x T hxS hTS hxT IH
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : ¬x ∈ T
IH : ↑(factorization (Finset.prod T g)) p = ↑(∑ x in T, factorization (g x)) p
hT : Finset.prod T g ≠ 0
⊢ ↑(factorization (Finset.prod (insert x T) g)) p = ↑(∑ x in insert x T, factorization (g x)) p
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : ¬x ∈ T
IH : ↑(factorization (Finset.prod T g)) p = ↑(∑ x in T, factorization (g x)) p
⊢ ↑(factorization (Finset.prod (insert x T) g)) p = ↑(∑ x in insert x T, factorization (g x)) p
have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
no goals
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : ¬x ∈ T
IH : ↑(factorization (Finset.prod T g)) p = ↑(∑ x in T, factorization (g x)) p
hT : Finset.prod T g ≠ 0
⊢ ↑(factorization (Finset.prod (insert x T) g)) p = ↑(∑ x in insert x T, factorization (g x)) p
simp [prod_insert hxT, sum_insert hxT, ← IH, factorization_mul (hS x hxS) hT]