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

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

case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i ((insert p S).prod id) = ∏ p ∈ insert p S, homogenization i p

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

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

State before:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p) * homogenization i (∏ x ∈ S, id x) = homogenization i p * ∏ p ∈ S, homogenization i p
Tactic:
rw [hSi]
State after:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p) * ∏ p ∈ S, homogenization i p = homogenization i p * ∏ p ∈ S, homogenization i p

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

State before:
case empty
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
⊢ homogenization i (∅.prod id) = ∏ p ∈ ∅, homogenization i p
Tactic:
simp
State after:
no goals