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'
⊢ Eq (α := MvPolynomial ι k) (Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) 0) 0

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
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'
⊢ F'' ≠ 0

Tactic:
have hF''0 : F'' ≠ 0 := ne_of_ne_of_eq ((Finsupp.mapDomain_injective fun s t h ↦ Subtype.ext
    (Finsupp.ext fun i ↦ by rw [hσ' _ s.2, hσ' _ t.2, h])).ne_iff.mpr hF'0) (by 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
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
h :
  ∀ (v : ↥F.support),
    Eq.{u_2 + 1} (α := K)
      (((AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) ∘ₗ
              Finsupp.lsingle v :
            (a : k) → K)
          1 :
        K)
      (((Finsupp.linearCombination k fun (s : ↥F.support) ↦
                (aeval a : (a : MvPolynomial ι k) → K)
                  ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1)) ∘ₗ
              Finsupp.lsingle v :
            (a : k) → K)
          1 :
        K)
⊢ Eq (α := Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K)
    (AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ))
    (Finsupp.linearCombination k fun (s : ↥F.support) ↦
      (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1))

Tactic:
ext v
-- 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
v : ↥F.support
⊢ Eq.{u_2 + 1} (α := K)
    (((AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) ∘ₗ
            Finsupp.lsingle v :
          (a : k) → K)
        1 :
      K)
    (((Finsupp.linearCombination k fun (s : ↥F.support) ↦
              (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1)) ∘ₗ
            Finsupp.lsingle v :
          (a : k) → K)
        1 :
      K)

Tactic:
simp [AddMonoidAlgebra, monomial]

Premises used: MvPolynomial.monomial, AddMonoidAlgebra
-- 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
⊢ Eq (α := Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K)
    (AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ))
    (Finsupp.linearCombination k fun (s : ↥F.support) ↦
      (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1))

Tactic:
have : (aeval a).toLinearMap ∘ₗ (Finsupp.lmapDomain k k fun s : F.support ↦ σ' s) =
        (Finsupp.linearCombination k fun s : F.support ↦ aeval a (monomial (σ' s) (1 : k))) := by
      ext v; simp [AddMonoidAlgebra, monomial]
-- 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_1 : ∀ (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
this :
  Eq (α := Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K)
    (AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ))
    (Finsupp.linearCombination k fun (s : ↥F.support) ↦
      (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1))
simp :
  Eq.{u_2 + 1} (α := K)
    ((aeval a : (a : MvPolynomial ι k) → K) (Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F') : K)
    (((AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ) :
            Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
⊢ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)

Tactic:
simp only [← hF', F'', ← 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_1 : ∀ (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
this :
  Eq (α := Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K)
    (AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ))
    (Finsupp.linearCombination k fun (s : ↥F.support) ↦
      (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1))
⊢ Eq.{u_2 + 1} (α := K)
    ((aeval a : (a : MvPolynomial ι k) → K) (Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F') : K)
    (((AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ) :
            Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)

Tactic:
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
⊢ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)

Tactic:
have hF'' : aeval a F'' = 0 := by
    have : (aeval a).toLinearMap ∘ₗ (Finsupp.lmapDomain k k fun s : F.support ↦ σ' s) =
        (Finsupp.linearCombination k fun s : F.support ↦ aeval a (monomial (σ' s) (1 : k))) := by
      ext v; simp [AddMonoidAlgebra, monomial]
    simp only [← hF', F'', ← this]; 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)
hpm : p * F''.totalDegree ≤ F.totalDegree
contrapose : ∀ (hF''0 : F''.totalDegree = 0), F'' = 0
⊢ F''.totalDegree ≠ 0

Tactic:
contrapose hF''0
-- 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'' : 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
⊢ coeff 0 F'' = 0

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''

Premises used: map_eq_zero, MvPolynomial.totalDegree_eq_zero_iff_eq_C, MvPolynomial.aeval_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
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'' : 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
hF''₁ : coeff 0 F'' = 0
⊢ p * F''.totalDegree ≤ F.totalDegree

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''

Premises used: map_eq_zero, MvPolynomial.totalDegree_eq_zero_iff_eq_C, MvPolynomial.aeval_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
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'' : 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
hF''₁ : coeff 0 F'' = 0
hpm₁ : p * F''.totalDegree ≤ F.totalDegree
⊢ F''.totalDegree = 0

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''

Premises used: map_eq_zero, MvPolynomial.totalDegree_eq_zero_iff_eq_C, MvPolynomial.aeval_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
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'' : coeff 0 F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
rw :
  Eq (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) (coeff 0 F'') : MvPolynomial ι k) (0 : MvPolynomial ι k)
rw₁ : Eq (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) 0) 0
rw₂ rw₃ : Eq (α := MvPolynomial ι k) 0 0
⊢ F'' = 0

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]

Premises used: map_zero, 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
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
⊢ F''.totalDegree ≠ 0

Tactic:
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]