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
σ : ι →₀ ℕ
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₀.coeff ((σ : (a : ι) → ℕ) i) = 0
e : ι ≃ Option { b : ι // b ≠ i } := (Equiv.optionSubtypeNe i).symm
⊢ coeff (Finsupp.equivMapDomain e σ).some
      (F₀.coeff ((Finsupp.equivMapDomain e σ : (a : Option { b : ι // b ≠ i }) → ℕ) none)) =
    coeff (Finsupp.equivMapDomain e σ)
      ((renameEquiv k e : (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k) F)

Tactic:
have : coeff _ (F₀.coeff _) = _ :=
      optionEquivLeft_coeff_some_coeff_none _ _ (σ.equivMapDomain e) (renameEquiv k e F)
-- 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₀.coeff ((σ : (a : ι) → ℕ) i) = 0
e : ι ≃ Option { b : ι // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  Eq.{u_1 + 1} (α := k)
    (coeff (Finsupp.equivMapDomain e σ).some
      (Polynomial.coeff
        ((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))
        ((Finsupp.equivMapDomain e σ : (a : Option { b : ι // b ≠ i }) → ℕ) none)))
    (coeff (Finsupp.equivMapDomain e σ)
      ((renameEquiv k e : (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k) F))
⊢ σ ∉ F.support

Tactic:
rw [renameEquiv_apply, Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _
      e.injective, Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Equiv.optionSubtypeNe_none,
      ← renameEquiv_apply, H, coeff_zero, eq_comm, ← notMem_support_iff] at this

Premises used: MvPolynomial.notMem_support_iff, Equiv.symm_symm, MvPolynomial.renameEquiv_apply, MvPolynomial.coeff_rename_mapDomain, eq_comm, Finsupp.equivMapDomain_eq_mapDomain, MvPolynomial.coeff_zero, Finsupp.mapDomain_equiv_apply, Equiv.injective, Equiv.optionSubtypeNe_none
-- 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₀.coeff ((σ : (a : ι) → ℕ) i) = 0
e : ι ≃ Option { b : ι // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this : σ ∉ F.support
⊢ False

Tactic:
this 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₀.coeff ((σ : (a : ι) → ℕ) i) = 0
e : ι ≃ Option { b : ι // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this : σ ∉ F.support
⊢ False

Tactic:
exact this 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 :
  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)
⊢ Eq (α := K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) :
      K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K) 0 : K)

Tactic:
apply_fun Subalgebra.val _ at H

Premises used: Subalgebra.val
-- 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 : ℕ)
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 :
  Eq (α := K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) :
      K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K) 0 : K)
⊢ Eq (α := K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        ((aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯ :
            (a_1 : MvPolynomial { j : ι // j ≠ i } k) → ↥(Algebra.adjoin k (a '' {i}ᶜ)))
          (Polynomial.coeff
            ((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))
            ((σ : (a : ι) → ℕ) i))) :
      K)
    (0 : K)

Tactic:
simp_rw [toPolynomialAdjoinImageCompl, Polynomial.coe_mapAlgHom, Polynomial.coeff_map,
      AlgHom.coe_toRingHom, map_zero] at H

Premises used: AlgHom.coe_toRingHom, Polynomial.coeff_map, MvPolynomial.toPolynomialAdjoinImageCompl, map_zero, Polynomial.coe_mapAlgHom
-- 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 : ℕ)
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 :
  Eq (α := K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        ((aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯ :
            (a_1 : MvPolynomial { j : ι // j ≠ i } k) → ↥(Algebra.adjoin k (a '' {i}ᶜ)))
          (Polynomial.coeff
            ((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))
            ((σ : (a : ι) → ℕ) i))) :
      K)
    (0 : K)
refine_2 :
  Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (aeval a) (rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i))) :
          (a : MvPolynomial { b : ι // b ≠ i } k) → K)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
      K)
    ((AlgHom.comp (B := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)))
            (aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯) :
          (a : MvPolynomial { j : ι // j ≠ i } k) → K)
        (Polynomial.coeff
          ((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))
          ((σ : (a : ι) → ℕ) i)) :
      K)
⊢ 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)

Tactic:
simp_rw [← H, ← AlgHom.comp_apply]

Premises used: AlgHom.comp_apply
-- 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 : ℕ)
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 :
  Eq (α := K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        ((aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯ :
            (a_1 : MvPolynomial { j : ι // j ≠ i } k) → ↥(Algebra.adjoin k (a '' {i}ᶜ)))
          (Polynomial.coeff
            ((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))
            ((σ : (a : ι) → ℕ) i))) :
      K)
    (0 : K)
refine_2 :
  Eq (α := MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k →ₐ[k] K)
    (AlgHom.comp (aeval a) (rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i))))
    (AlgHom.comp (B := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)))
      (aeval fun (j : { j : ι // j ≠ i }) ↦
        Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
          (a (↑j : ι)) ⋯))
⊢ Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (aeval a) (rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i))) :
          (a : MvPolynomial { b : ι // b ≠ i } k) → K)
        (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
      K)
    ((AlgHom.comp (B := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)))
            (aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯) :
          (a : MvPolynomial { j : ι // j ≠ i } k) → K)
        (Polynomial.coeff
          ((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))
          ((σ : (a : ι) → ℕ) i)) :
      K)

Tactic:
congr
-- 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 : ℕ)
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 :
  Eq (α := K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        ((aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯ :
            (a_1 : MvPolynomial { j : ι // j ≠ i } k) → ↥(Algebra.adjoin k (a '' {i}ᶜ)))
          (Polynomial.coeff
            ((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))
            ((σ : (a : ι) → ℕ) i))) :
      K)
    (0 : K)
refine_2 :
  ∀ (i_1 : { b : ι // b ≠ i }),
    Eq.{u_2 + 1} (α := K)
      ((AlgHom.comp (aeval a) (rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i))) :
            (a : MvPolynomial { b : ι // b ≠ i } k) → K)
          (X i_1) :
        K)
      ((AlgHom.comp (B := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)))
              (aeval fun (j : { j : ι // j ≠ i }) ↦
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                  (a (↑j : ι)) ⋯) :
            (a : MvPolynomial { b : ι // b ≠ i } k) → K)
          (X i_1) :
        K)
⊢ Eq (α := MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k →ₐ[k] K)
    (AlgHom.comp (aeval a) (rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i))))
    (AlgHom.comp (B := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)))
      (aeval fun (j : { j : ι // j ≠ i }) ↦
        Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
          (a (↑j : ι)) ⋯))

Tactic:
ext
-- 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 : ℕ)
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 :
  Eq (α := K)
    ((Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)) : (a : ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        ((aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯ :
            (a_1 : MvPolynomial { j : ι // j ≠ i } k) → ↥(Algebra.adjoin k (a '' {i}ᶜ)))
          (Polynomial.coeff
            ((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))
            ((σ : (a : ι) → ℕ) i))) :
      K)
    (0 : K)
i_1 : { b : ι // b ≠ i }
⊢ Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (aeval a) (rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i))) :
          (a : MvPolynomial { b : ι // b ≠ i } k) → K)
        (X i_1) :
      K)
    ((AlgHom.comp (B := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Subalgebra.val (Algebra.adjoin k (a '' {i}ᶜ)))
            (aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯) :
          (a : MvPolynomial { b : ι // b ≠ i } k) → K)
        (X i_1) :
      K)

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
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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
hi : i ∈ F.vars
have : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support) (hσi : i ∈ σ.support), IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
have ⟨σ, hσ, hσi⟩ := (mem_vars_iff_mem_support i).mp hi
-- 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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
hi : i ∈ F.vars
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hσi : i ∈ σ.support
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
⟨toPolynomialAdjoinImageCompl F a i,
    fun h ↦ coeff_toPolynomialAdjoinImageCompl_ne_zero HF σ hσ i
      (Finsupp.mem_support_iff.mp hσi) ?_, aeval_toPolynomialAdjoinImageCompl_eq_zero hFa ..⟩

Premises used: Finsupp.mem_support_iff, IsAlgebraic, MvPolynomial.toPolynomialAdjoinImageCompl, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, And.intro, Exists.intro, Iff.mp, MvPolynomial.coeff_toPolynomialAdjoinImageCompl_ne_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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
hi : i ∈ F.vars
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hσi : i ∈ σ.support
refine :
  ∀ (h : Eq (α := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i) 0),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
refine ⟨toPolynomialAdjoinImageCompl F a i,
    fun h ↦ coeff_toPolynomialAdjoinImageCompl_ne_zero HF σ hσ i
      (Finsupp.mem_support_iff.mp hσi) ?_, aeval_toPolynomialAdjoinImageCompl_eq_zero hFa ..⟩
-- 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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
hi : i ∈ F.vars
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hσi : i ∈ σ.support
h : Eq (α := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i) 0
rw : Eq.{u_2 + 1} (α := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Polynomial.coeff 0 ((σ : (a : ι) → ℕ) i)) 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := ↥(Algebra.adjoin k (a '' {i}ᶜ))) 0 0
⊢ Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0

Tactic:
rw [h, Polynomial.coeff_zero]

Premises used: Polynomial.coeff_zero