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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
⊢ homogenization i p ≠ 0
Tactic:
intro h
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ False

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ False
Tactic:
apply hp
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ p = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ p = 0
Tactic:
refine' Finsupp.mapDomain_injOn _ this _ _ h
State after:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ p ∈ {w | ↑w.support ⊆ {w | w i = 0}}

case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ 0 ∈ {w | ↑w.support ⊆ {w | w i = 0}}

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
Tactic:
intro t ht y hy hh
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t ∈ {w | w i = 0}
y : ι →₀ ℕ
hy : y ∈ {w | w i = 0}
hh :
  (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) t =
    (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) y
⊢ t = y

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t ∈ {w | w i = 0}
y : ι →₀ ℕ
hy : y ∈ {w | w i = 0}
hh :
  (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) t =
    (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) y
⊢ t = y
Tactic:
simp only [Set.mem_setOf_eq] at hh hy ht
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
⊢ t = y

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
⊢ t = y
Tactic:
ext a
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
⊢ t a = y a

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
⊢ t a = y a
Tactic:
have :
  (t + Finsupp.single i (p.totalDegree - t.sum fun _ m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun _ m => m)) a :=
  by rw [hh]
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t + Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t + Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a
Tactic:
simp only [Finsupp.coe_add, Pi.add_apply] at this
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  t a + (Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    y a + (Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
⊢ (t + Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
Tactic:
rw [hh]
State after:
no goals

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  t a + (Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    y a + (Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a
Tactic:
rw [Finsupp.single_apply, Finsupp.single_apply] at this
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t a + if i = a then p.totalDegree - t.sum fun x m => m else 0) =
    y a + if i = a then p.totalDegree - y.sum fun x m => m else 0
⊢ t a = y a

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t a + if i = a then p.totalDegree - t.sum fun x m => m else 0) =
    y a + if i = a then p.totalDegree - y.sum fun x m => m else 0
⊢ t a = y a
Tactic:
split_ifs at this  with hia
State after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : i = a
this : t a + (p.totalDegree - t.sum fun x m => m) = y a + (p.totalDegree - y.sum fun x m => m)
⊢ t a = y a

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : ¬i = a
this : t a + 0 = y a + 0
⊢ t a = y a

State before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : i = a
this : t a + (p.totalDegree - t.sum fun x m => m) = y a + (p.totalDegree - y.sum fun x m => m)
⊢ t a = y a
Tactic:
rw [← hia, ht, hy]
State after:
no goals

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : ¬i = a
this : t a + 0 = y a + 0
⊢ t a = y a
Tactic:
simpa
State after:
no goals

State before:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ p ∈ {w | ↑w.support ⊆ {w | w i = 0}}
Tactic:
intro x hx
State after:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑p.support
⊢ x ∈ {w | w i = 0}

State before:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑p.support
⊢ x ∈ {w | w i = 0}
Tactic:
rw [Set.mem_setOf_eq, hjp x hx]
State after:
no goals

State before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ 0 ∈ {w | ↑w.support ⊆ {w | w i = 0}}
Tactic:
simp only [Set.mem_setOf_eq]
State after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ ↑(Finsupp.support 0) ⊆ {w | w i = 0}

State before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ ↑(Finsupp.support 0) ⊆ {w | w i = 0}
Tactic:
intro x hx
State after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑(Finsupp.support 0)
⊢ x ∈ {w | w i = 0}

State before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑(Finsupp.support 0)
⊢ x ∈ {w | w i = 0}
Tactic:
simp only [mem_coe, Finsupp.mem_support_iff, ne_eq] at hx
State after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 x = 0
⊢ x ∈ {w | w i = 0}

State before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 x = 0
⊢ x ∈ {w | w i = 0}
Tactic:
change ¬ 0 = 0 at hx
State after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 = 0
⊢ x ∈ {w | w i = 0}

State before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 = 0
⊢ x ∈ {w | w i = 0}
Tactic:
simp only [not_true] at hx
State after:
no goals