-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem prod {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ι → M) {w : σ → M} :
    (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
      IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)

Tactic:
exact h j (Finset.mem_insert_of_mem hjs)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ ∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)

Tactic:
intro j hjs

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous w (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)

Tactic:
intro i s his IH h

Result:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)

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

Tactic:
refine Finset.induction_on s ?_ ?_

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

case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous w (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)

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

Tactic:
simp only [isWeightedHomogeneous_one, Finset.sum_empty, Finset.prod_empty]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (φ i * ∏ i ∈ s, φ i) (n i + ∑ i ∈ s, n i)

Tactic:
apply (h i (Finset.mem_insert_self _ _)).mul (IH _)

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ ∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)

Tactic:
simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]

Result:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (φ i * ∏ i ∈ s, φ i) (n i + ∑ i ∈ s, n i)

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

Tactic:
intro

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