awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
⊢ PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits

Tactic:
⟨fun ⟨h⟩ f hf ↦ ?_, fun h ↦ ?_⟩

Premises used: _private.0.perfectField_iff_splits_of_natSepDegree_eq_one.match_1, Iff.intro, Polynomial.Splits
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
refine_1 :
  PerfectField F → ∀ (f : F[X]) (hf : f.natSepDegree = 1) (h : ∀ {f : F[X]}, Irreducible f → f.Separable), f.Splits
refine_2 : ∀ (h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits), PerfectField F
⊢ PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits

Tactic:
refine ⟨fun ⟨h⟩ f hf ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
⊢ f ≠ 0

Tactic:
aesop
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
⊢ f ≠ 0

Tactic:
have hf0 : f ≠ 0 := by aesop
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
refine_1 : ∀ (u : F[X]ˣ) (hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f), f.Splits
⊢ f.Splits

Tactic:
obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hf0

Premises used: UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
refine_1 : ((UniqueFactorizationMonoid.factors f).prod * (↑u : F[X])).Splits
⊢ f.Splits

Tactic:
rw [← hu]
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
⊢ ((UniqueFactorizationMonoid.factors f).prod * (↑u : F[X])).Splits

Tactic:
(Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits

Premises used: Polynomial.Splits.multisetProd, IsUnit.splits, Units.isUnit, Polynomial.Splits.mul
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
refine_1 : ∀ (g : F[X]) (hg : g ∈ UniqueFactorizationMonoid.factors f), g.Splits
⊢ ((UniqueFactorizationMonoid.factors f).prod * (↑u : F[X])).Splits

Tactic:
refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits

Premises used: Polynomial.Splits.multisetProd, IsUnit.splits, Units.isUnit, Polynomial.Splits.mul
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
⊢ g.Separable

Tactic:
specialize h (UniqueFactorizationMonoid.irreducible_of_factor g hg)

Premises used: UniqueFactorizationMonoid.irreducible_of_factor
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
h : g.Separable
⊢ g.natSepDegree ≤ f.natSepDegree

Tactic:
have key := natSepDegree_le_of_dvd g f (UniqueFactorizationMonoid.dvd_of_mem_factors hg) hf0
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
h : g.Separable
key : g.natSepDegree ≤ f.natSepDegree
⊢ g.natDegree ≤ 1

Tactic:
rw [h.natSepDegree_eq_natDegree, hf] at key

Premises used: Polynomial.Separable.natSepDegree_eq_natDegree
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
h : g.Separable
key : g.natDegree ≤ 1
⊢ g.Splits

Tactic:
Splits.of_natDegree_le_one key

Premises used: Polynomial.Splits.of_natDegree_le_one
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
h : g.Separable
key : g.natDegree ≤ 1
⊢ g.Splits

Tactic:
exact Splits.of_natDegree_le_one key

Premises used: Polynomial.Splits.of_natDegree_le_one
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
refine_2 : ∀ (p : ℕ), ExpChar F p → PerfectField F
⊢ PerfectField F

Tactic:
obtain ⟨p, _⟩ := ExpChar.exists F

Premises used: ExpChar.exists
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x : F
obtain :
  ∀ (y : F) (hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0),
    ∃ (a : F), (frobenius F p : (a : F) → F) a = x
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x

Tactic:
obtain ⟨y, hy⟩ := Splits.exists_eval_eq_zero
      (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
      ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'

Premises used: Polynomial.Splits.exists_eval_eq_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x y : F
hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0
rwa :
  ∀ (hy : eval y (HPow.hPow (α := F[X]) X p) - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
rwa₁ : ∀ (hy : y ^ p - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
rwa₂ : ∀ (hy : y ^ p - x = 0), (frobenius F p : (a : F) → F) y = x
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hy : y ^ p = x), (frobenius F p : (a : F) → F) y = x
⊢ (frobenius F p : (a : F) → F) y = x

Tactic:
rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy

Premises used: Polynomial.eval_C, sub_eq_zero, Polynomial.eval_X_pow, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x y : F
hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x

Tactic:
exact ⟨y, by rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
⊢ PerfectRing F p

Tactic:
haveI := PerfectRing.ofSurjective F p fun x ↦ by
    obtain ⟨y, hy⟩ := Splits.exists_eval_eq_zero
      (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
      ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'
    exact ⟨y, by rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
this : PerfectRing F p
⊢ PerfectField F

Tactic:
PerfectRing.toPerfectField F p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
this : PerfectRing F p
⊢ PerfectField F

Tactic:
exact PerfectRing.toPerfectField F p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
E : Type v
inst : Field E
K : Type w
inst_1 : Field K
inst_2 : PerfectField K
f : E[X]
i : E →+* K
hf : f.natSepDegree = 1
⊢ (Polynomial.map i f).Splits

Tactic:
(perfectField_iff_splits_of_natSepDegree_eq_one K).mp ‹_› _ (natSepDegree_map K f i ▸ hf)

Premises used: Polynomial.natSepDegree_map, Eq.rec, perfectField_iff_splits_of_natSepDegree_eq_one, Iff.mp, Eq.symm
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
rw :
  Eq (α := K)
    ((AlgHom.restrictScalars k (Polynomial.aeval (a i)) : (a : Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        (F.toPolynomialAdjoinImageCompl a i) :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) F : K)
⊢ Eq (α := K)
    ((Polynomial.aeval (a i) : (a : Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        (F.toPolynomialAdjoinImageCompl a i) :
      K)
    (0 : K)

Tactic:
rw [← hFa, ← AlgHom.restrictScalars_apply k]

Premises used: AlgHom.restrictScalars_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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
simp_rw :
  Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
            (AlgHom.comp
              (Polynomial.mapAlgHom
                (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 : ι)) ⋯))
              (AlgHom.comp
                (↑(optionEquivLeft k { b : ι // b ≠ i }) :
                  MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
                (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
                  MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))) :
          (a : MvPolynomial ι k) → K)
        F :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) F : K)
⊢ Eq (α := K)
    ((AlgHom.restrictScalars k (Polynomial.aeval (a i)) : (a : Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        (F.toPolynomialAdjoinImageCompl a i) :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) F : K)

Tactic:
simp_rw [toPolynomialAdjoinImageCompl, ← AlgEquiv.coe_algHom, ← AlgHom.comp_apply]

Premises used: MvPolynomial.toPolynomialAdjoinImageCompl, AlgHom.comp_apply, AlgEquiv.coe_algHom
-- 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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
e_a :
  Eq (α := MvPolynomial ι k →ₐ[k] K)
    (AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
      (AlgHom.comp
        (Polynomial.mapAlgHom
          (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 : ι)) ⋯))
        (AlgHom.comp
          (↑(optionEquivLeft k { b : ι // b ≠ i }) :
            MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
          (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
            MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))))
    (aeval a)
⊢ Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
            (AlgHom.comp
              (Polynomial.mapAlgHom
                (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 : ι)) ⋯))
              (AlgHom.comp
                (↑(optionEquivLeft k { b : ι // b ≠ i }) :
                  MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
                (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
                  MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))) :
          (a : MvPolynomial ι k) → K)
        F :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) F : 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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
e_a :
  ∀ (i_1 : ι),
    Eq.{u_2 + 1} (α := K)
      ((AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
              (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
              (AlgHom.comp
                (Polynomial.mapAlgHom
                  (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 : ι)) ⋯))
                (AlgHom.comp
                  (↑(optionEquivLeft k { b : ι // b ≠ i }) :
                    MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
                  (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
                    MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))) :
            (a : MvPolynomial ι k) → K)
          (X i_1) :
        K)
      ((aeval a : (a : MvPolynomial ι k) → K) (X i_1) : K)
⊢ Eq (α := MvPolynomial ι k →ₐ[k] K)
    (AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
      (AlgHom.comp
        (Polynomial.mapAlgHom
          (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 : ι)) ⋯))
        (AlgHom.comp
          (↑(optionEquivLeft k { b : ι // b ≠ i }) :
            MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
          (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
            MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))))
    (aeval a)

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
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i i_1 : ι
⊢ Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
            (AlgHom.comp
              (Polynomial.mapAlgHom
                (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 : ι)) ⋯))
              (AlgHom.comp
                (↑(optionEquivLeft k { b : ι // b ≠ i }) :
                  MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
                (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
                  MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))) :
          (a : MvPolynomial ι k) → K)
        (X i_1) :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) (X i_1) : K)

Tactic:
aesop (add simp optionEquivLeft_X_some) (add simp optionEquivLeft_X_none)

Premises used: MvPolynomial.optionEquivLeft_X_some, MvPolynomial.optionEquivLeft_X_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 : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
h :
  ∀ (x : K),
    x ∈ a '' {i}ᶜ ↔ Membership.mem (γ := Set K) (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)) x
⊢ a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)

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 : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
x : K
⊢ x ∈ a '' {i}ᶜ ↔ Membership.mem (γ := Set K) (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)) x

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 : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
⊢ a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)

Tactic:
have : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; 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 : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
this : a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
⊢ Irreducible.{u_2} (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    ((Polynomial.mapAlgEquiv
            (H.aevalEquiv.trans
              (Subalgebra.equivOfEq (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
                (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)) :
          (a_1 : Polynomial (MvPolynomial { b : ι // b ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        ((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)) :
      Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))

Tactic:
hF.map (renameEquiv k (Equiv.optionSubtypeNe i).symm) |>.map (optionEquivLeft k _) |>.map
      (Polynomial.mapAlgEquiv
        (H.aevalEquiv.trans (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $this.symm))))

Premises used: congrArg, Subalgebra.equivOfEq, Algebra.adjoin, id, AlgebraicIndependent.aevalEquiv, Irreducible.map, AlgEquiv.trans, Equiv.optionSubtypeNe, MvPolynomial.optionEquivLeft, Equiv.symm, Polynomial.mapAlgEquiv, Eq.symm, MvPolynomial.renameEquiv
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
this : a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
h :
  Eq (α :=
    (a_1 : Polynomial (MvPolynomial.{u_3, u_1} { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (⇑(Polynomial.mapAlgHom
          (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 : Polynomial (MvPolynomial { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (⇑(Polynomial.mapAlgEquiv
          (H.aevalEquiv.trans
            (Subalgebra.equivOfEq (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
              (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))) :
      (a_1 : Polynomial (MvPolynomial { b : ι // b ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
⊢ Irreducible.{u_2} (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    ((Polynomial.mapAlgHom
            (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 : Polynomial (MvPolynomial { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        ((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)) :
      Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))

Tactic:
convert!
    hF.map (renameEquiv k (Equiv.optionSubtypeNe i).symm) |>.map (optionEquivLeft k _) |>.map
      (Polynomial.mapAlgEquiv
        (H.aevalEquiv.trans (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $this.symm))))
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
this : a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
h :
  (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 : ι))
        ⋯) =
    (↑(H.aevalEquiv.trans
          (Subalgebra.equivOfEq (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
            (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)) :
      MvPolynomial (↑{j : ι | j ≠ i} : Type u_3) k →ₐ[k] ↥(Algebra.adjoin k (a '' {i}ᶜ)))
⊢ Eq (α :=
    (a_1 : Polynomial (MvPolynomial.{u_3, u_1} { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (⇑(Polynomial.mapAlgHom
          (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 : Polynomial (MvPolynomial { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (⇑(↑(Polynomial.mapAlgEquiv
              (H.aevalEquiv.trans
                (Subalgebra.equivOfEq
                  (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
                  (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))) :
          Polynomial (MvPolynomial { b : ι // b ≠ i } k) →ₐ[k] Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) :
      (a_1 : Polynomial (MvPolynomial { b : ι // b ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))

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 : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
this : a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
⊢ (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 : ι))
        ⋯) =
    (↑(H.aevalEquiv.trans
          (Subalgebra.equivOfEq (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
            (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)) :
      MvPolynomial (↑{j : ι | j ≠ i} : Type u_3) k →ₐ[k] ↥(Algebra.adjoin k (a '' {i}ᶜ)))

Tactic:
aesop