awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
refine_1 : Algebra.IsAlgebraic.{u_1, u_2} F ↥(⨅ (i : ι), t i)
⊢ Normal.{u_1, u_2} F ↥(⨅ (i : ι), t i)
have refine_2 : ∀ (x : ↥(⨅ (i : ι), t i)),
  Splits.{u_2} (R := ↥(⨅ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨅ (i : ι), t i)) (minpoly F x))
Tactic: refine { toIsAlgebraic := ?_, splits' := fun x => ?_ }
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
i : ι
⊢ Splits.{u_2} (R := ↥(t i)) (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x))
have rw : Splits.{u_2} (R := ↥(t i))
  (Polynomial.map (algebraMap F ↥(t i)) (minpoly F (B := ↥(t i)) ((inclusion sorry : (a : ↥(iInf t)) → ↥(t i)) x : ↥(t i))))
Tactic: rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
⊢ Splits.{u_2} (R := ↥(⨅ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨅ (i : ι), t i)) (minpoly F x))
have hx : ∀ (i : ι), Splits.{u_2} (R := ↥(t i)) (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x))
Tactic: have hx : ∀ i, Splits ((minpoly F x).map (algebraMap F (t i))) := by
      intro i
      rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]
      exact (h i).splits' (inclusion (iInf_le t i) x)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
hx : ∀ (i : ι), Splits.{u_2} (R := ↥(t i)) (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x))
⊢ Splits.{u_2} (R := ↥(⨅ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨅ (i : ι), t i)) (minpoly F x))
have refine_2 : ∀ (hx : ∀ (i : ι), ∀ x_1 ∈ rootSet (minpoly F x) K, x_1 ∈ t i),
  ∀ x_1 ∈ rootSet (minpoly F x) K, Membership.mem (γ := IntermediateField F K) (⨅ (i : ι), t i) x_1
Tactic: simp only [splits_iff_mem (Splits.of_isScalarTower K (hx hι.some))] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
⊢ f.fieldRange = E
have rw : (E.val.comp (↑g : ↥E →ₐ[F] ↥E)).fieldRange = E
Tactic: rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
    ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
    IntermediateField.fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
rw : (E.val.comp (↑g : ↥E →ₐ[F] ↥E)).fieldRange = E
⊢ f.fieldRange = E
have rw₁ : IntermediateField.map E.val (↑g : ↥E →ₐ[F] ↥E).fieldRange = E
Tactic: rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
    ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
    IntermediateField.fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
rw : (E.val.comp (↑g : ↥E →ₐ[F] ↥E)).fieldRange = E
rw₁ : IntermediateField.map E.val (↑g : ↥E →ₐ[F] ↥E).fieldRange = E
⊢ f.fieldRange = E
have rw₂ : IntermediateField.map E.val ⊤ = E
Tactic: rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
    ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
    IntermediateField.fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
rw : (E.val.comp (↑g : ↥E →ₐ[F] ↥E)).fieldRange = E
rw₁ : IntermediateField.map E.val (↑g : ↥E →ₐ[F] ↥E).fieldRange = E
rw₂ : IntermediateField.map E.val ⊤ = E
⊢ f.fieldRange = E
have rw₃ : E.val.fieldRange = E
Tactic: rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
    ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
    IntermediateField.fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
rw : (E.val.comp (↑g : ↥E →ₐ[F] ↥E)).fieldRange = E
rw₁ : IntermediateField.map E.val (↑g : ↥E →ₐ[F] ↥E).fieldRange = E
rw₂ : IntermediateField.map E.val ⊤ = E
rw₃ : E.val.fieldRange = E
⊢ f.fieldRange = E
have rw₄ : E = E
Tactic: rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
    ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
    IntermediateField.fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_6
inst_1 : Field E
inst_2 : Algebra F E
h : Normal F E
x y : E
⊢ Eq (α := F[X]) (minpoly F x) (minpoly F y) ↔ x ∈ MulAction.orbit Gal(E/F) y
have refine : ∀ (he : Eq (α := F[X]) (minpoly F x) (minpoly F y)), x ∈ MulAction.orbit Gal(E/F) y
Tactic: refine ⟨fun he ↦ ?_, fun ⟨f, he⟩ ↦ he ▸ minpoly.algEquiv_eq f y⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_6
inst_1 : Field E
inst_2 : Algebra F E
h : Normal F E
x y : E
he : Eq (α := F[X]) (minpoly F x) (minpoly F y)
⊢ x ∈ MulAction.orbit Gal(E/F) y
have obtain : ∀ (φ : E →ₐ[F] E) (hφ : (φ : (a : E) → E) y = x), x ∈ MulAction.orbit Gal(E/F) y
Tactic: obtain ⟨φ, hφ⟩ := exists_algHom_of_splits_of_aeval (normal_iff.mp h) (he ▸ minpoly.aeval F x)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
inst_7 : Normal F K₁
h1 : IsSolvable.{u_3} Gal(K₁/F)
h2 : IsSolvable.{u_6} Gal(E/K₁)
f : Gal(E/K₁) →* Gal(E/F) :=
  {
    toFun := fun (ϕ : Gal(E/K₁)) ↦
      AlgEquiv.ofAlgHom (AlgHom.restrictScalars F (↑ϕ : E →ₐ[K₁] E)) (AlgHom.restrictScalars F (↑ϕ.symm : E →ₐ[K₁] E)) ⋯
        ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ IsSolvable.{u_6} Gal(E/F)
have solvable_of_ker_le_range : ∀ (ϕ : Gal(E/F))
  (hϕ : Membership.mem (γ := Subgroup Gal(E/F)) (MonoidHom.ker (M := Gal(K₁/F)) (AlgEquiv.restrictNormalHom K₁)) ϕ)
  (x : K₁), ϕ.toFun ((algebraMap K₁ E : (a : K₁) → E) x) = (algebraMap K₁ E : (a : K₁) → E) x
Tactic: refine
    solvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
      ⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) x = y
have hx : IsAlgebraic K x
Tactic: have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
⊢ (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y
have rw : (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) ((f : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯) = y
Tactic: rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
rw : (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) ((f : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯) = y
⊢ (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y
have rw₁ : (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (AdjoinSimple.gen K y) = y
Tactic: rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
rw : (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) ((f : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯) = y
rw₁ : (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (AdjoinSimple.gen K y) = y
⊢ (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y
have rw₂ : y = y
Tactic: rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) x = y
have hxy : (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y
Tactic: have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by
    rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x
have obtain : ∀ (σ : Gal(L/K)) (hσ : (σ : (a : L) → L) x = y), ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x
Tactic: obtain ⟨σ, hσ⟩ := exists_algEquiv_of_root hy h_ev
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
σ : Gal(L/K)
hσ : (σ : (a : L) → L) x = y
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x
have h : (σ.symm : (a : L) → L) y = x
Tactic: use σ.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
σ : Gal(L/K)
hσ : (σ : (a : L) → L) x = y
⊢ (σ.symm : (a : L) → L) y = x
have h : (σ.symm : (a : L) → L) ((σ : (a : L) → L) x : L) = x
Tactic: rw [← hσ, symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
σ : Gal(L/K)
hσ : (σ : (a : L) → L) x = y
h : (σ.symm : (a : L) → L) ((σ : (a : L) → L) x : L) = x
⊢ (σ.symm : (a : L) → L) y = x
have h₁ : x = x
Tactic: rw [← hσ, symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
inst_2 : Algebra F_1 K_1
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F_1 K₁
inst_7 : Algebra F_1 K₂
inst_8 : Algebra F_1 K₃
ϕ : K₁ →ₐ[F_1] K₂
χ : K₁ ≃ₐ[F_1] K₂
ψ : K₂ →ₐ[F_1] K₃
ω : K₂ ≃ₐ[F_1] K₃
F : Type u_6
K : Type u_7
inst_9 : Field F
inst_10 : Field K
inst_11 : Algebra F K
inst_12 : IsQuadraticExtension F K
x : K
⊢ Splits (map (algebraMap F K) (minpoly F x))
have inl : ∀ (h : natDegree (minpoly F x) < 2), Splits (map (algebraMap F K) (minpoly F x))
Tactic: obtain h | h := le_iff_lt_or_eq.mp (finrank_eq_two F K ▸ minpoly.natDegree_le x)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
inst_2 : Algebra F_1 K_1
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F_1 K₁
inst_7 : Algebra F_1 K₂
inst_8 : Algebra F_1 K₃
ϕ : K₁ →ₐ[F_1] K₂
χ : K₁ ≃ₐ[F_1] K₂
ψ : K₂ →ₐ[F_1] K₃
ω : K₂ ≃ₐ[F_1] K₃
F : Type u_6
K : Type u_7
inst_9 : Field F
inst_10 : Field K
inst_11 : Algebra F K
inst_12 : IsQuadraticExtension F K
x : K
inl : ∀ (h : natDegree (minpoly F x) < 2), Splits (map (algebraMap F K) (minpoly F x))
⊢ Splits (map (algebraMap F K) (minpoly F x))
have inr : ∀ (h : natDegree (minpoly F x) = 2), Splits (map (algebraMap F K) (minpoly F x))
Tactic: obtain h | h := le_iff_lt_or_eq.mp (finrank_eq_two F K ▸ minpoly.natDegree_le x)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
⊢ x_1 ∈ rootSet (minpoly F x) L
have rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
Tactic: rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
⊢ x_1 ∈ rootSet (minpoly F x) L
have rw₁ : Eq.{u_3 + 1} (α := L) (((aeval ((f.toRingHom : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
  (0 : L)
Tactic: rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₁ :
  Eq.{u_3 + 1} (α := L) (((aeval ((f.toRingHom : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
⊢ x_1 ∈ rootSet (minpoly F x) L
have rw₂ : Eq.{u_3 + 1} (α := L) (((aeval (((↑f : K →+* L) : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
  (0 : L)
Tactic: rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₁ :
  Eq.{u_3 + 1} (α := L) (((aeval ((f.toRingHom : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₂ :
  Eq.{u_3 + 1} (α := L) (((aeval (((↑f : K →+* L) : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
⊢ x_1 ∈ rootSet (minpoly F x) L
have rw₃ : Eq.{u_3 + 1} (α := L) (((aeval ((f : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
Tactic: rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₁ :
  Eq.{u_3 + 1} (α := L) (((aeval ((f.toRingHom : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₂ :
  Eq.{u_3 + 1} (α := L) (((aeval (((↑f : K →+* L) : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₃ : Eq.{u_3 + 1} (α := L) (((aeval ((f : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
⊢ x_1 ∈ rootSet (minpoly F x) L
have rw₄ : Eq.{u_3 + 1} (α := L) ((f : (a : K) → L) ((aeval x : (a : F[X]) → K) (minpoly F x) : K) : L) (0 : L)
Tactic: rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₁ :
  Eq.{u_3 + 1} (α := L) (((aeval ((f.toRingHom : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₂ :
  Eq.{u_3 + 1} (α := L) (((aeval (((↑f : K →+* L) : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₃ : Eq.{u_3 + 1} (α := L) (((aeval ((f : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₄ : Eq.{u_3 + 1} (α := L) ((f : (a : K) → L) ((aeval x : (a : F[X]) → K) (minpoly F x) : K) : L) (0 : L)
⊢ x_1 ∈ rootSet (minpoly F x) L
have rw₅ : Eq.{u_3 + 1} (α := L) ((f : (a : K) → L) 0 : L) (0 : L)
Tactic: rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₁ :
  Eq.{u_3 + 1} (α := L) (((aeval ((f.toRingHom : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₂ :
  Eq.{u_3 + 1} (α := L) (((aeval (((↑f : K →+* L) : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₃ : Eq.{u_3 + 1} (α := L) (((aeval ((f : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₄ : Eq.{u_3 + 1} (α := L) ((f : (a : K) → L) ((aeval x : (a : F[X]) → K) (minpoly F x) : K) : L) (0 : L)
rw₅ : Eq.{u_3 + 1} (α := L) ((f : (a : K) → L) 0 : L) (0 : L)
⊢ x_1 ∈ rootSet (minpoly F x) L
have rw₆ : Eq.{u_3 + 1} (α := L) 0 0
Tactic: rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
⊢ IsNormalClosure F K L ↔
    (∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))) ∧
      Eq (α := IntermediateField F L) (normalClosure F K L) ⊤
have refine_1 : IsNormalClosure F K L →
  ∀ (splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x)))
    (h : Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)) ⊤),
    Eq (α := IntermediateField F L) (normalClosure F K L) ⊤
Tactic: refine ⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
refine_1 :
  IsNormalClosure F K L →
    ∀ (splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x)))
      (h :
        Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)) ⊤),
      Eq (α := IntermediateField F L) (normalClosure F K L) ⊤
⊢ IsNormalClosure F K L ↔
    (∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))) ∧
      Eq (α := IntermediateField F L) (normalClosure F K L) ⊤
have refine_2 : (∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))) ∧
    Eq (α := IntermediateField F L) (normalClosure F K L) ⊤ →
  ∀ (splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x)))
    (h : Eq (α := IntermediateField F L) (normalClosure F K L) ⊤),
    Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)) ⊤
Tactic: refine ⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)
have rw : (∀ (x : K),
    Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))) ∧
  Eq.{u_3 + 1} (α := IntermediateField F ↥(normalClosure F K L)) (normalClosure F K ↥(normalClosure F K L)) ⊤
Tactic: rw [isNormalClosure_iff]