case refine_1
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ (∀ (i : ι), i ∈ ∅ → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in ∅, φ i) (∑ i in ∅, n i)

case refine_2
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)) →
        (∀ (i : ι), i ∈ insert a s → IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous w (∏ i in insert a s, φ i) (∑ i in insert a s, n i)
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
refine Finset.induction_on s ?_ ?_
case refine_1
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
a✝ : ∀ (i : ι), i ∈ ∅ → IsWeightedHomogeneous w (φ i) (n i)
⊢ IsWeightedHomogeneous w (∏ i in ∅, φ i) (∑ i in ∅, n i)
case refine_1
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ (∀ (i : ι), i ∈ ∅ → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in ∅, φ i) (∑ i in ∅, n i)
intro
no goals
case refine_1
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
a✝ : ∀ (i : ι), i ∈ ∅ → IsWeightedHomogeneous w (φ i) (n i)
⊢ IsWeightedHomogeneous w (∏ i in ∅, φ i) (∑ i in ∅, n i)
simp only [isWeightedHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
case refine_2
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (∏ i in insert i s, φ i) (∑ i in insert i s, n i)
case refine_2
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)) →
        (∀ (i : ι), i ∈ insert a s → IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous w (∏ i in insert a s, φ i) (∑ i in insert a s, n i)
intro i s his IH h
case refine_2
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (φ i * ∏ i in s, φ i) (n i + ∑ i in s, n i)
case refine_2
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (∏ 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]
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ ∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)
case refine_2
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (φ i * ∏ i in s, φ i) (n i + ∑ i in s, n i)
apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ ∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)
intro j hjs
no goals
R : Type u_3
M : Type u_4
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ✝ ψ : MvPolynomial σ R
m n✝ : M
ι : Type u_1
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)
exact h j (Finset.mem_insert_of_mem hjs)