σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)
⊢ IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
revert h
case refine'_1
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ (i : ι), i ∈ ∅ → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in ∅, φ i) (∑ i in ∅, n i)

case refine'_2
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)) →
        (∀ (i : ι), i ∈ insert a s → IsHomogeneous (φ i) (n i)) →
          IsHomogeneous (∏ i in insert a s, φ i) (∑ i in insert a s, n i)
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
refine' Finset.induction_on s _ _
case refine'_1
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h✝ : ∀ (i : ι), i ∈ ∅ → IsHomogeneous (φ i) (n i)
⊢ IsHomogeneous (∏ i in ∅, φ i) (∑ i in ∅, n i)
case refine'_1
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ (i : ι), i ∈ ∅ → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in ∅, φ i) (∑ i in ∅, n i)
intro
no goals
case refine'_1
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h✝ : ∀ (i : ι), i ∈ ∅ → IsHomogeneous (φ i) (n i)
⊢ IsHomogeneous (∏ i in ∅, φ i) (∑ i in ∅, n i)
simp only [isHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
case refine'_2
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ IsHomogeneous (∏ i in insert i s, φ i) (∑ i in insert i s, n i)
case refine'_2
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)) →
        (∀ (i : ι), i ∈ insert a s → IsHomogeneous (φ i) (n i)) →
          IsHomogeneous (∏ i in insert a s, φ i) (∑ i in insert a s, n i)
intro i s his IH h
case refine'_2
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ IsHomogeneous (φ i * ∏ i in s, φ i) (n i + ∑ i in s, n i)
case refine'_2
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ IsHomogeneous (∏ i in insert i s, φ i) (∑ i in insert i s, n i)
simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ ∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)
case refine'_2
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ IsHomogeneous (φ i * ∏ i in s, φ i) (n i + ∑ i in s, n i)
apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsHomogeneous (φ j) (n j)
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ ∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)
intro j hjs
no goals
σ : Type u_2
τ : Type ?u.161634
R : Type u_3
S : Type ?u.161640
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsHomogeneous (φ j) (n j)
exact h j (Finset.mem_insert_of_mem hjs)