awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ False
have 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)
Tactic: have H := HF (rename (↑) (F₀.coeff (σ i))) ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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 ≤
    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)
have rw : (σ : (a : ι) → ℕ) i ≤ F.totalDegree
Tactic: rw [totalDegree_renameEquiv]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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)))
⊢ False
have 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)
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σ)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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)
⊢ False
have this₁ : HAdd.hAdd (β := ℕ) (F₀.coeff ((σ : (a : ι) → ℕ) i)).totalDegree ((σ : (a : ι) → ℕ) i : ℕ) ≤ F.totalDegree
Tactic: rw [totalDegree_renameEquiv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
have refine_1 : ∀ (H : F₀.coeff ((σ : (a : ι) → ℕ) i) = 0), False
Tactic: refine (map_eq_zero_iff _ (rename_injective _ Subtype.val_injective)).not.mpr fun H ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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
⊢ False
have this : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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))
⊢ False
have this₁ : σ ∉ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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.{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)
have 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)
Tactic: apply_fun Subalgebra.val _ at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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.{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)
have 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 : ι)) sorry :
          (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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ 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)
have 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 : ι)) sorry) :
        (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: simp_rw [← H, ← AlgHom.comp_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ 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)
have 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 : ι))
        sorry))
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ 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 : ι)) ⋯))
have 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 : ι)) sorry) :
          (a : MvPolynomial { b : ι // b ≠ i } k) → K)
        (X i_1) :
      K)
Tactic: ext