Theorem: MvPolynomial.homogenization_prod (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : σ → MvPolynomial ι S
L : Finset σ
⊢ homogenization i (∏ l ∈ L, P l) = ∏ l ∈ L, homogenization i (P l)
Tactic:
induction' L using Finset.induction with p S hS hSi
State after:
case empty
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : σ → MvPolynomial ι S
⊢ homogenization i (∏ l ∈ ∅, P l) = ∏ l ∈ ∅, homogenization i (P l)

case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (∏ l ∈ insert p S, P l) = ∏ l ∈ insert p S, homogenization i (P l)

State before:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (∏ l ∈ insert p S, P l) = ∏ l ∈ insert p S, homogenization i (P l)
Tactic:
simp only [Finset.prod_insert hS]
State after:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p * ∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)

State before:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p * ∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)
Tactic:
rw [homogenization_mul]
State after:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p) * homogenization i (∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)

State before:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p) * homogenization i (∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)
Tactic:
rw [hSi]
State after:
no goals

State before:
case empty
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : σ → MvPolynomial ι S
⊢ homogenization i (∏ l ∈ ∅, P l) = ∏ l ∈ ∅, homogenization i (P l)
Tactic:
simp
State after:
no goals