awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ (∀ (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)) ⊤
have left : ∀ (x : K),
  Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))
Tactic: constructor
-- 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))
left :
  ∀ (x : K),
    Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))
⊢ (∀ (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)) ⊤
have right : Eq.{u_3 + 1} (α := IntermediateField F ↥(normalClosure F K L)) (normalClosure F K ↥(normalClosure F K L)) ⊤
Tactic: constructor
-- 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))
⊢ ∀ (x : K),
    Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))
have left : ∀ (x : K),
  Splits.{u_3} (R := ↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)))
    (Polynomial.map (algebraMap F ↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L))) (minpoly F x))
Tactic: rw [normalClosure_eq_iSup_adjoin_of_splits 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))
⊢ Eq.{u_3 + 1} (α := IntermediateField F ↥(normalClosure F K L)) (normalClosure F K ↥(normalClosure F K L)) ⊤
have right : LE.le.{u_3} (α := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤
  (⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange)
Tactic: simp_rw [normalClosure, ← top_le_iff]
-- 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))
⊢ LE.le.{u_3} (α := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤
    (⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange)
have right : ∀ (x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
  Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x →
    Membership.mem (α := L) (γ := Set L)
      ((⇑(AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange))) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) ''
        (↑(⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange) :
          Set ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)))
      ((AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)
Tactic: refine fun x _ ↦ ((⨆ f : K →ₐ[F] L, f.fieldRange).val).injective.mem_set_image |>.mp ?_
-- 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))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
⊢ Membership.mem (α := L) (γ := Set L)
    ((⇑(AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange))) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) ''
      (↑(⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange) :
        Set ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)))
    ((AlgHom.toRingHom (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)
have right : Membership.mem (α := L)
  (↑(⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
        IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange) :
    Set L)
  ((val (⨆ (f : K →ₐ[F] L), f.fieldRange) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)
Tactic: rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_val, ← IntermediateField.coe_val,
    ← IntermediateField.coe_map, IntermediateField.map_iSup]
-- 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))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
⊢ Membership.mem (α := L)
    (↑(⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
          IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange) :
      Set L)
    ((val (⨆ (f : K →ₐ[F] L), f.fieldRange) : (a : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) → L) x : L)
have right : ∀ (f : K →ₐ[F] L),
  f.fieldRange ≤
    ⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
      IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange
Tactic: refine (iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2
-- 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))
x : ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)
h : Membership.mem (γ := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤ x
f : K →ₐ[F] L
⊢ f.fieldRange ≤
    ⨆ (i : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)),
      IntermediateField.map (val (⨆ (f : K →ₐ[F] L), f.fieldRange)) i.fieldRange
have right : f.fieldRange ≤
  IntermediateField.map (L := ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) (val (⨆ (f : K →ₐ[F] L), f.fieldRange))
    (AlgHom.fieldRange (f.codRestrict (toSubalgebra (⨆ (f : K →ₐ[F] L), f.fieldRange)) sorry))
Tactic: refine le_iSup_of_le (f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (hypothesis)
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
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
⊢ L →ₐ[F] L'
have this : Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L)) ⊤
Tactic: have := h.adjoin_rootSet
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (hypothesis)
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
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L)) ⊤
⊢ L →ₐ[F] L'
have this₁ : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
Tactic: rw [← gc.l_iSup] at this
Cleared hypotheses: this
-- 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
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
⊢ L →ₐ[F] L'
have refine : ∀ (x : L) (hx : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x),
  Splits (Polynomial.map (algebraMap F L') (minpoly F x))
Tactic: refine Nonempty.some <| nonempty_algHom_of_adjoin_splits
    (fun x hx ↦ ⟨isAlgebraic_iff_isIntegral.mp ((h.normal).isAlgebraic x), ?_⟩) this
-- 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
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))
have obtain : ∀ (y : K) (hx : x ∈ rootSet (minpoly F y) L), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
Tactic: obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
-- 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
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx_1 : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
y : K
hx : x ∈ rootSet (minpoly F y) L
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))
have pos : ∀ (iy : IsIntegral F y), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
Tactic: by_cases iy : IsIntegral F y
-- 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
h : IsNormalClosure F K L
L' : Type u_4
inst_5 : Field L'
inst_6 : Algebra F L'
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
this : Eq.{u_3 + 1} (α := IntermediateField F L) (adjoin F (⨆ (x : K), rootSet (minpoly F x) L)) ⊤
x : L
hx_1 : Membership.mem (γ := Set L) (⨆ (x : K), rootSet (minpoly F x) L) x
y : K
hx : x ∈ rootSet (minpoly F y) L
pos : ∀ (iy : IsIntegral F y), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
⊢ Splits (Polynomial.map (algebraMap F L') (minpoly F x))
have neg : ∀ (iy : ¬IsIntegral F y), Splits (Polynomial.map (algebraMap F L') (minpoly F x))
Tactic: by_cases iy : IsIntegral F y
-- 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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
⊢ IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)
have have : ∀ (φ : K →ₐ[F] L), IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)
Tactic: have ⟨φ⟩ := ne
-- 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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)
have apply : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: apply (h.toIsAlgebraic.of_injective φ φ.injective).isNormalClosure_normalClosure
-- 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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have simp_rw : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly.{u_1, u_3} F (B := L) ((φ : (a : K) → L) x : L)))
Tactic: simp_rw [← minpoly.algHom_eq _ φ.injective]
-- 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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))
have have : ∀ (φ : K →ₐ[F] L), Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))
Tactic: have ⟨φ⟩ := ne
-- 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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (x : K), adjoin F (rootSet (minpoly F x) L))
have refine : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: refine h.toIsAlgebraic.of_injective φ φ.injective
    |>.normalClosure_eq_iSup_adjoin_of_splits fun 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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have rw : Splits (Polynomial.map (algebraMap F L) (minpoly.{u_1, u_3} F (B := L) ((φ : (a : K) → L) x : L)))
Tactic: rw [← minpoly.algHom_eq _ φ.injective]
-- 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
h : Normal F L
⊢ Normal.{u_1, u_3} F ↥(normalClosure F K L)
have inl : IsEmpty (K →ₐ[F] L) → Normal.{u_1, u_3} F ↥(normalClosure F K L)
Tactic: obtain _ | φ := isEmpty_or_nonempty (K →ₐ[F] L)
-- 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
h : Normal F L
inl : IsEmpty (K →ₐ[F] L) → Normal.{u_1, u_3} F ↥(normalClosure F K L)
⊢ Normal.{u_1, u_3} F ↥(normalClosure F K L)
have inr : ∀ (φ : Nonempty (K →ₐ[F] L)), Normal.{u_1, u_3} F ↥(normalClosure F K L)
Tactic: obtain _ | φ := isEmpty_or_nonempty (K →ₐ[F] L)
-- 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
h : Normal F L
h_1 : IsEmpty (K →ₐ[F] L)
⊢ Normal.{u_1, u_3} F ↥(normalClosure F K L)
have inl : Normal.{u_1, u_3} F ↥⊥
Tactic: rw [normalClosure, iSup_of_empty]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (hypothesis)
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 : FiniteDimensional F K
⊢ FiniteDimensional.{u_1, u_3} F ↥(normalClosure F K L)
have this : ∀ (f : K →ₐ[F] L), FiniteDimensional.{u_1, u_3} F ↥f.fieldRange
Tactic: haveI : ∀ f : K →ₐ[F] L, FiniteDimensional F f.fieldRange := fun f ↦
    f.toLinearMap.finiteDimensional_range
-- 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 K L
inst_6 : IsScalarTower F K L
⊢ IsScalarTower.{u_1, u_2, u_3} F K ↥(normalClosure F K L)
have h : Eq (α := RingHom.{u_1, u_3} F ↥(normalClosure F K L)) (algebraMap F ↥(normalClosure F K L))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K ↥(normalClosure F K L)) (algebraMap F K))
Tactic: apply of_algebraMap_eq'
-- 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 K L
inst_6 : IsScalarTower F K L
⊢ Eq (α := RingHom.{u_1, u_3} F ↥(normalClosure F K L)) (algebraMap F ↥(normalClosure F K L))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K ↥(normalClosure F K L)) (algebraMap F K))
have h : ∀ (x : F),
  Eq.{u_3 + 1} (α := L) (↑((algebraMap F ↥(normalClosure F K L) : (a : F) → ↥(normalClosure F K L)) x) : L)
    (↑((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K ↥(normalClosure F K L)) (algebraMap F K) :
            (a : F) → ↥(normalClosure F K L))
          x) :
      L)
Tactic: ext 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
⊢ Nonempty (AlgHom.{u_1, u_4, u_3} F (↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L'))) L)
have rw : Nonempty (AlgHom.{u_1, u_4, u_3} F (↥(IntermediateField.adjoin F (⨆ (x : K), rootSet (minpoly F x) L'))) L)
Tactic: rw [← gc.l_iSup]
-- 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
⊢ Nonempty (AlgHom.{u_1, u_4, u_3} F (↥(IntermediateField.adjoin F (⨆ (x : K), rootSet (minpoly F x) L'))) L)
have refine : ∀ (x : L') (hx : Membership.mem (γ := Set L') (⨆ (x : K), rootSet (minpoly F x) L') x),
  IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: refine nonempty_algHom_adjoin_of_splits fun x hx ↦ ?_
-- 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
x : L'
hx : Membership.mem (γ := Set L') (⨆ (x : K), rootSet (minpoly F x) L') x
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have obtain : ∀ (y : K) (hx : x ∈ rootSet (minpoly F y) L'), IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
-- 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
x : L'
hx_1 : Membership.mem (γ := Set L') (⨆ (x : K), rootSet (minpoly F x) L') x
y : K
hx : x ∈ rootSet (minpoly F y) L'
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have refine : Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: refine ⟨isAlgebraic_iff_isIntegral.mp (isAlgebraic_of_mem_rootSet hx), ?_⟩
-- 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
x : L'
hx_1 : Membership.mem (γ := Set L') (⨆ (x : K), rootSet (minpoly F x) L') x
y : K
hx : x ∈ rootSet (minpoly F y) L'
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have pos : ∀ (iy : IsIntegral F y), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: by_cases iy : IsIntegral F y
-- 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
h : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
x : L'
hx_1 : Membership.mem (γ := Set L') (⨆ (x : K), rootSet (minpoly F x) L') x
y : K
hx : x ∈ rootSet (minpoly F y) L'
pos : ∀ (iy : IsIntegral F y), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
have neg : ∀ (iy : ¬IsIntegral F y), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
Tactic: by_cases iy : IsIntegral F y
-- 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
h_1 : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
L' : Type u_4
inst_6 : Field L'
inst_7 : Algebra F L'
φ : AlgHom.{u_1, u_4, u_3} F (↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L'))) L := Nonempty.some ⋯
φ' : AlgHom.{u_1, u_4, u_3} F (↥(normalClosure F K L')) L := φ.comp (inclusion ⋯)
x x_1 : K →ₐ[F] L'
h :
  Eq (α := K →ₐ[F] L)
    ((φ'.comp ∘ (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
      x)
    ((φ'.comp ∘ (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
      x_1)
⊢ Eq (α := AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L'))
    ((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x :
      AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L'))
    ((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x_1 :
      AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L'))
have rw : ∀
  (h :
    Eq (α := (a : K) → L)
      (⇑((φ'.comp ∘
              (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
            x) :
        (a : K) → L)
      (⇑((φ'.comp ∘
              (⇑(Equiv.symm (normalClosure.algHomEquiv F K L')) : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')))
            x_1) :
        (a : K) → L)),
  Eq (α := (a : K) → ↥(normalClosure F K L'))
    (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x :
          AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
      (a : K) → ↥(normalClosure F K L'))
    (⇑((Equiv.symm (normalClosure.algHomEquiv F K L') : (a : K →ₐ[F] L') → K →ₐ[F] ↥(normalClosure F K L')) x_1 :
          AlgHom.{u_1, u_2, u_4} F K ↥(normalClosure F K L')) :
      (a : K) → ↥(normalClosure F K L'))
Tactic: rw [DFunLike.ext'_iff] at h ⊢
Cleared hypotheses: h