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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0' : F''.totalDegree ≠ 0
⊢ p * F''.totalDegree ≤ 1 * F''.totalDegree

Tactic:
replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).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
p : ℕ
hp : Nat.Prime p
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)
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0' : F''.totalDegree ≠ 0
this : p * F''.totalDegree ≤ 1 * F''.totalDegree
⊢ False

Tactic:
hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp this)

Premises used: mul_le_mul_iff_of_pos_right, Nat.Prime.one_lt, Iff.mp, LT.lt.not_ge, Ne.bot_lt
-- 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
p : ℕ
hp : Nat.Prime p
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)
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0' : F''.totalDegree ≠ 0
this : p * F''.totalDegree ≤ 1 * F''.totalDegree
⊢ False

Tactic:
exact hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp this)

Premises used: mul_le_mul_iff_of_pos_right, Nat.Prime.one_lt, Iff.mp, LT.lt.not_ge, Ne.bot_lt
-- 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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
suffices : p * F''.totalDegree ≤ F.totalDegree
⊢ False

Tactic:
suffices hpm : p * F''.totalDegree ≤ F.totalDegree by
    have hF''0' : F''.totalDegree ≠ 0 := by
      contrapose hF''0
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
    replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).symm)
    exact hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp 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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
rw : ∀ b ∈ F''.support, (p * b.sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree
⊢ p * F''.totalDegree ≤ F.totalDegree

Tactic:
rw [totalDegree, Finset.mul_sup₀, Finset.sup_le_iff]

Premises used: MvPolynomial.totalDegree, Finset.sup_le_iff, Finset.mul_sup₀
-- 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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ι →₀ ℕ
hσ : σ ∈ F''.support
obtain :
  ∀ (σ : ↥F.support) (hσ₂ : σ ∈ F'.support) (hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support),
    (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree
⊢ (p * σ.sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree

Tactic:
obtain ⟨σ, hσ₂, rfl⟩ := Finset.mem_image.mp (Finsupp.mapDomain_support hσ)

Premises used: Finset.mem_image, Finsupp.mapDomain_support, Iff.mp, rfl
-- 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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
⊢ (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree

Tactic:
le_trans ?_ (Finset.le_sup σ.2)

Premises used: Subtype.property, Finset.le_sup, 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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
refine : (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
⊢ (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree

Tactic:
refine le_trans ?_ (Finset.le_sup σ.2)

Premises used: Subtype.property, Finset.le_sup, 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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
rw : p * (σ' (↑σ : ι →₀ ℕ)).sum fun (i : ι) (a : ℕ) ↦ a
| (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e

Tactic:
rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]

Premises used: Finsupp.sum_smul_index, Finsupp.mul_sum, Subtype.property
-- 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
p : ℕ
hp : Nat.Prime p
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)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
H :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
conv_rhs : (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
conv_rhs₁ : (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e
⊢ (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e

Tactic:
conv_rhs => rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]

Premises used: Finsupp.sum_smul_index, Finsupp.mul_sum, Subtype.property
-- 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
suffices : S.Nonempty
⊢ ∃ F ∈ S,
    ∀ (G : MvPolynomial ι k),
      G ≠ 0 →
        Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) G : K) (0 : K) → F.totalDegree ≤ G.totalDegree

Tactic:
suffices S.Nonempty from
      ⟨totalDegree.argminOn S this, totalDegree.argminOn_mem ..,
        fun _ h₁ h₂ ↦ totalDegree.argminOn_le S ⟨h₁, 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
this : ¬AlgebraicIndependent k a
⊢ S.Nonempty

Tactic:
simpa [S, algebraicIndependent_iff, and_comm] using this

Premises used: algebraicIndependent_iff, and_comm
-- 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
suffices : ¬AlgebraicIndependent k a
⊢ S.Nonempty

Tactic:
suffices ¬ AlgebraicIndependent k a by simpa [S, algebraicIndependent_iff, and_comm] using 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
⊢ n ∉ {n}ᶜ

Tactic:
simp
-- 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
refine : IsAlgebraic (↥(Algebra.adjoin k (a '' {n}ᶜ))) (a n)
⊢ False

Tactic:
refine h.transcendental_adjoin (i := n) (s := {n}ᶜ) (by simp) ?_

Premises used: AlgebraicIndependent.transcendental_adjoin
-- 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
⊢ a '' {n}ᶜ = Set.range fun (x : { i : ι // i ≠ n }) ↦ a (↑x : ι)

Tactic:
aesop
-- 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
⊢ a '' {n}ᶜ = Set.range fun (x : { i : ι // i ≠ n }) ↦ a (↑x : ι)

Tactic:
have : a '' {n}ᶜ = Set.range (ι := {i // i ≠ n}) (a ·) := by aesop
-- 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
this : a '' {n}ᶜ = Set.range fun (x : { i : ι // i ≠ n }) ↦ a (↑x : ι)
⊢ IsAlgebraic (↥(Algebra.adjoin k (Set.range fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)))) (a n)

Tactic:
ha'.isAlgebraic.isAlgebraic _

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- 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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
this : a '' {n}ᶜ = Set.range fun (x : { i : ι // i ≠ n }) ↦ a (↑x : ι)
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {n}ᶜ))) (a n)

Tactic:
convert! ha'.isAlgebraic.isAlgebraic _

Premises used: Algebra.IsAlgebraic.isAlgebraic