awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
⊢ Irreducible F

Tactic:
⟨fun h' ↦ (h'.map (aeval a)).ne_zero hFa, fun q₁ q₂ e ↦ ?_⟩

Premises used: MvPolynomial.aeval, Irreducible.mk, IsUnit.ne_zero, IsUnit.map
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
refine : ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂), IsUnit q₁ ∨ IsUnit q₂
⊢ Irreducible F

Tactic:
refine ⟨fun h' ↦ (h'.map (aeval a)).ne_zero hFa, fun q₁ q₂ e ↦ ?_⟩
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
inr :
  ∀
    (this :
      ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂)
        (h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂)
    (h₁ : ¬Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂
wlog :
  ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂)
    (h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
wlog h₁ : aeval a q₁ = 0 generalizing q₁ q₂

Premises used: MvPolynomial.aeval, DFunLike.coe
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
this :
  ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂)
    (h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂
h₁ : ¬Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₂ : K) (0 : K)

Tactic:
simpa [h₁, hFa] using Eq.symm <| congr(aeval a $e)

Premises used: Eq.symm
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
this :
  ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂)
    (h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂
h₁ : ¬Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
exact .symm (this q₂ q₁ (e.trans (mul_comm ..)) <| by
      simpa [h₁, hFa] using Eq.symm <| congr(aeval a $e))
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
⊢ q₁ ≠ 0 ∧ q₂ ≠ 0

Tactic:
have ne := mul_ne_zero_iff.mp (e ▸ hF0)
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
⊢ F.totalDegree ≤ q₁.totalDegree

Tactic:
have := HF q₁ ne.1 h₁
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : F.totalDegree ≤ q₁.totalDegree
⊢ q₂.totalDegree = 0

Tactic:
rw [e, totalDegree_mul_of_isDomain ne.1 ne.2, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this

Premises used: add_le_iff_nonpos_right, MvPolynomial.totalDegree_mul_of_isDomain, And.right, And.left, nonpos_iff_eq_zero
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
.inr (isUnit_iff_totalDegree_of_isReduced.mpr ⟨?_, this⟩)

Premises used: Iff.mpr, MvPolynomial.isUnit_iff_totalDegree_of_isReduced, And.intro, Or.inr
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
refine : IsUnit (coeff 0 q₂)
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
refine .inr (isUnit_iff_totalDegree_of_isReduced.mpr ⟨?_, this⟩)
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
⊢ q₁ ≠ 0 ∧
    Ne (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) (coeff 0 q₂) : MvPolynomial ι k) (0 : MvPolynomial ι k)

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp this] at ne

Premises used: MvPolynomial.totalDegree_eq_zero_iff_eq_C, Iff.mp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
ne₁ :
  q₁ ≠ 0 ∧
    Ne (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) (coeff 0 q₂) : MvPolynomial ι k) (0 : MvPolynomial ι k)
⊢ q₂.totalDegree = 0

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp this] at ne

Premises used: MvPolynomial.totalDegree_eq_zero_iff_eq_C, Iff.mp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne :
  q₁ ≠ 0 ∧
    Ne (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) (coeff 0 q₂) : MvPolynomial ι k) (0 : MvPolynomial ι k)
this : q₂.totalDegree = 0
⊢ IsUnit (coeff 0 q₂)

Tactic:
simpa using ne.2

Premises used: And.right
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
refine_3 :
  ∀
    (H :
      F.totalDegree ≤
        totalDegree.{u_1, u_3} (R := k) (σ := ι)
          ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) :
              (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
            (F₀.coeff ((σ : (a : ι) → ℕ) i)))),
    False
refine_1 :
  Ne (α := MvPolynomial ι k)
    ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
      MvPolynomial ι k)
    (0 : MvPolynomial ι k)
refine_2 :
  Eq.{u_2 + 1} (α := K)
    ((aeval a : (a : MvPolynomial ι k) → K)
        ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
            (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
          MvPolynomial ι k) :
      K)
    (0 : K)
⊢ False

Tactic:
have H := HF (rename (↑) (F₀.coeff (σ i))) ?_ ?_
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H_1 :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
H :
  F.totalDegree ≤
    totalDegree.{u_1, u_3} (R := k) (σ := ι)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)))
rw : (σ : (a : ι) → ℕ) i ≤ F.totalDegree
⊢ (σ : (a : ι) → ℕ) i ≤
    totalDegree.{u_1, u_3} (R := k) (σ := Option { b : ι // b ≠ i })
      ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
          (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
        F)

Tactic:
rw [totalDegree_renameEquiv]

Premises used: MvPolynomial.totalDegree_renameEquiv
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H_1 :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
H :
  F.totalDegree ≤
    totalDegree.{u_1, u_3} (R := k) (σ := ι)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)))
⊢ (σ : (a : ι) → ℕ) i ≤ F.totalDegree

Tactic:
(Finsupp.le_degree ..).trans (le_totalDegree hσ)

Premises used: Finsupp.le_degree, MvPolynomial.le_totalDegree, LE.le.trans
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H_1 :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
H :
  F.totalDegree ≤
    totalDegree.{u_1, u_3} (R := k) (σ := ι)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)))
⊢ (σ : (a : ι) → ℕ) i ≤ F.totalDegree

Tactic:
exact (Finsupp.le_degree ..).trans (le_totalDegree hσ)

Premises used: Finsupp.le_degree, MvPolynomial.le_totalDegree, LE.le.trans
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H_1 :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
H :
  F.totalDegree ≤
    totalDegree.{u_1, u_3} (R := k) (σ := ι)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)))
⊢ HAdd.hAdd (β := ℕ) (F₀.coeff ((σ : (a : ι) → ℕ) i)).totalDegree ((σ : (a : ι) → ℕ) i : ℕ) ≤
    totalDegree.{u_1, u_3} (R := k) (σ := Option { b : ι // b ≠ i })
      ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
          (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
        F)

Tactic:
have : (F₀.coeff (σ i)).totalDegree + σ i ≤ _ :=
      totalDegree_coeff_optionEquivLeft_add_le _ _ _ (σ i) <| by
        rw [totalDegree_renameEquiv]
        exact (Finsupp.le_degree ..).trans (le_totalDegree hσ)
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H_1 :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
H :
  F.totalDegree ≤
    totalDegree.{u_1, u_3} (R := k) (σ := ι)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)))
this :
  HAdd.hAdd (β := ℕ) (F₀.coeff ((σ : (a : ι) → ℕ) i)).totalDegree ((σ : (a : ι) → ℕ) i : ℕ) ≤
    totalDegree.{u_1, u_3} (R := k) (σ := Option { b : ι // b ≠ i })
      ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
          (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
        F)
⊢ HAdd.hAdd (β := ℕ) (F₀.coeff ((σ : (a : ι) → ℕ) i)).totalDegree ((σ : (a : ι) → ℕ) i : ℕ) ≤ F.totalDegree

Tactic:
rw [totalDegree_renameEquiv] at this

Premises used: MvPolynomial.totalDegree_renameEquiv
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H_1 :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
H :
  F.totalDegree ≤
    totalDegree.{u_1, u_3} (R := k) (σ := ι)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)))
this : HAdd.hAdd (β := ℕ) (F₀.coeff ((σ : (a : ι) → ℕ) i)).totalDegree ((σ : (a : ι) → ℕ) i : ℕ) ≤ F.totalDegree
⊢ False

Tactic:
simpa [hσi] using (this.trans H).trans (totalDegree_rename_le _ _)

Premises used: MvPolynomial.totalDegree_rename_le, LE.le.trans
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
⊢ Ne (α := MvPolynomial ι k)
    ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
      MvPolynomial ι k)
    (0 : MvPolynomial ι k)

Tactic:
(map_eq_zero_iff _ (rename_injective _ Subtype.val_injective)).not.mpr fun H ↦ ?_

Premises used: Iff.mpr, Subtype.val_injective, Iff.not, MvPolynomial.rename_injective, map_eq_zero_iff
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
refine_1 : ∀ (H : F₀.coeff ((σ : (a : ι) → ℕ) i) = 0), False
⊢ Ne (α := MvPolynomial ι k)
    ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
      MvPolynomial ι k)
    (0 : MvPolynomial ι k)

Tactic:
refine (map_eq_zero_iff _ (rename_injective _ Subtype.val_injective)).not.mpr fun H ↦ ?_

Premises used: Iff.mpr, Subtype.val_injective, Iff.not, MvPolynomial.rename_injective, map_eq_zero_iff