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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
⊢ homogenization i p = p
Tactic:
by_cases hpn : p = 0
State after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : p = 0
⊢ homogenization i p = p

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ homogenization i p = p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ homogenization i p = p
Tactic:
rw [homogenization]
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
have := (hp.totalDegree hpn).symm
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
this : n = p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
this : n = p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
subst this
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : p.IsHomogeneous p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : p.IsHomogeneous p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
rw [IsHomogeneous] at hp
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
have : ∀ (x) (_ : x ∈ p.support),
    (fun j : ι →₀ ℕ => j + Finsupp.single i (p.totalDegree - j.sum fun (_x : ι) (m : ℕ) => m))
        x = x := by
  intro x hx
  simp only [add_right_eq_self, Finsupp.single_eq_same, tsub_eq_zero_iff_le, Finsupp.single_tsub,
    Finsupp.single_le_iff]
  rw [← hp (mem_support_iff.mp hx), weightedDegree_one]
  exact le_refl _
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
rw [Finsupp.mapDomain_congr this]
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun x => x) p = p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun x => x) p = p
Tactic:
erw [Finsupp.mapDomain_id]
State after:
no goals

State before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : p = 0
⊢ homogenization i p = p
Tactic:
simp [hpn]
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
⊢ ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
Tactic:
intro x hx
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
Tactic:
simp only [add_right_eq_self, Finsupp.single_eq_same, tsub_eq_zero_iff_le, Finsupp.single_tsub,
  Finsupp.single_le_iff]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ p.totalDegree ≤ x.sum fun _x m => m

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ p.totalDegree ≤ x.sum fun _x m => m
Tactic:
rw [← hp (mem_support_iff.mp hx), weightedDegree_one]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ degree x ≤ x.sum fun _x m => m

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ degree x ≤ x.sum fun _x m => m
Tactic:
exact le_refl _
State after:
no goals