awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : L →ₐ[F] L), map f K)
have refine_1 : ∀ (f : ↥K →ₐ[F] L), f.fieldRange ≤ ⨆ (f : L →ₐ[F] L), map f K
Tactic: refine (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
refine_1 : ∀ (f : ↥K →ₐ[F] L), f.fieldRange ≤ ⨆ (f : L →ₐ[F] L), map f K
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : L →ₐ[F] L), map f K)
have refine_2 : ∀ (f : L →ₐ[F] L), map f K ≤ ⨆ (f : ↥K →ₐ[F] L), f.fieldRange
Tactic: refine (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K)
have refine_1 : ∀ (f : L →ₐ[F] L), map f K ≤ ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K
Tactic: refine (normalClosure_def' K).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K : IntermediateField F L
inst_3 : Normal F L
refine_1 : ∀ (f : L →ₐ[F] L), map f K ≤ ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥K) L) (⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K)
have refine_2 : ∀ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K ≤ ⨆ (f : L →ₐ[F] L), map f K
Tactic: refine (normalClosure_def' K).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
K K' : IntermediateField F L
inst_3 : Normal F L
h : K ≤ K'
⊢ LE.le (α := IntermediateField F L) (normalClosure F (↥K) L) (normalClosure F (↥K') L)
have rw : LE.le.{u_3} (α := IntermediateField F L) (⨆ (f : L →ₐ[F] L), map f K) (⨆ (f : L →ₐ[F] L), map f K')
Tactic: rw [normalClosure_def', normalClosure_def']
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
have rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
have rw₁ : ⨆ (f : ↥K →ₐ[F] L), f.fieldRange ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
rw₁ : ⨆ (f : ↥K →ₐ[F] L), f.fieldRange ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
have rw₂ : (∀ (i : ↥K →ₐ[F] L), i.fieldRange ≤ K) ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
have rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
have rw₁ : ⨆ (f : L →ₐ[F] L), map f K ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
rw₁ : ⨆ (f : L →ₐ[F] L), map f K ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
have rw₂ : (∀ (i : L →ₐ[F] L), map i K ≤ K) ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
have rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def'', iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
have rw₁ : ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def'', iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
rw : normalClosure F (↥K) L ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
rw₁ : ⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
⊢ Normal.{u_1, u_3} F ↥K ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
have rw₂ : (∀ (i : Gal(L/F)), map (↑i : L →ₐ[F] L) K ≤ K) ↔ ∀ (σ : Gal(L/F)), map (↑σ : L →ₐ[F] L) K ≤ K
Tactic: rw [normal_iff_normalClosure_le, normalClosure_def'', iSup_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
σ_1 : L →ₐ[F] L
σ : Gal(L/F)
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥(map (↑σ : L →ₐ[F] L) K)) L) (normalClosure F (↥K) L)
have simp_rw : Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (f : Gal(L/F)), map ((↑f : L →ₐ[F] L).comp (↑σ : L →ₐ[F] L)) K)
  (⨆ (f : Gal(L/F)), map (↑f : L →ₐ[F] L) K)
Tactic: simp_rw [normalClosure_def'', map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (hypothesis)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K : IntermediateField F L
σ : L →ₐ[F] L
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥(map σ K)) L) (normalClosure F (↥K) L)
have this : ∀ (σ : Gal(L/F)),
  Eq (α := IntermediateField F L) (normalClosure F (↥(map (↑σ : L →ₐ[F] L) K)) L) (normalClosure F (↥K) L)
Tactic: have (σ : Gal(L/F)) : normalClosure F (K.map (σ : L →ₐ[F] L)) L = normalClosure F K L := by
    simp_rw [normalClosure_def'', map_map]
    exact (Equiv.mulRight σ).iSup_congr fun _ ↦ rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K₁ K₂ : IntermediateField F L
inst_4 : Normal.{u_1, u_3} F ↥K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂
have refine_1 : ∀ (h : normalClosure F (↥K₁) L ≤ K₂), K₁ ≤ K₂
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K₁ K₂ : IntermediateField F L
inst_4 : Normal.{u_1, u_3} F ↥K₂
refine_1 : ∀ (h : normalClosure F (↥K₁) L ≤ K₂), K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂
have refine_2 : ∀ (h : K₁ ≤ K₂), normalClosure F (↥K₁) L ≤ K₂
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (hypothesis)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K₁ K₂ : IntermediateField F L
inst_4 : Normal.{u_1, u_3} F ↥K₂
h : normalClosure F (↥K₁) L ≤ K₂
⊢ K₁ ≤ K₂
have h₁ : ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂
Tactic: rw [normalClosure_le_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Closure (goal)
Goal:
F : Type u_1
L : Type u_3
inst : Field F
inst_1 : Field L
inst_2 : Algebra F L
inst_3 : Normal F L
K₁ K₂ : IntermediateField F L
inst_4 : Normal.{u_1, u_3} F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂
have refine_2 : LE.le (α := IntermediateField F L) (normalClosure F (↥K₁) L) (normalClosure F (↥K₂) L)
Tactic: rw [← normalClosure_of_normal K₂]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : Type u_3
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
h : Normal F E
x : E
⊢ IsIntegral K x ∧ Splits (map (algebraMap K E) (minpoly K x))
have hx : IsIntegral F x
Tactic: obtain ⟨hx, hhx⟩ := h.out x
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : Type u_3
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
⊢ IsIntegral K x ∧ Splits (map (algebraMap K E) (minpoly K x))
have hhx : Splits (map (algebraMap F E) (minpoly F x))
Tactic: obtain ⟨hx, hhx⟩ := h.out x
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : Type u_3
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits (map (algebraMap F E) (minpoly F x))
⊢ IsIntegral K x ∧ Splits (map (algebraMap K E) (minpoly K x))
have hhx₁ : Splits (map (algebraMap K E) (map (algebraMap F K) (minpoly F x)))
Tactic: rw [algebraMap_eq F K E, ← map_map] at hhx
Cleared hypotheses: hhx
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
E' : Type u_4
inst_3 : Field E'
inst_4 : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
⊢ Normal F E'
have rw : ∀ (h : ∀ (x : E), IsIntegral F x ∧ Splits (map (algebraMap F E) (minpoly F x))) (f : E ≃ₐ[F] E') (x : E'),
  IsIntegral F x ∧ Splits (map (algebraMap F E') (minpoly F x))
Tactic: rw [normal_iff] at h ⊢
Cleared hypotheses: h, f
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
E' : Type u_4
inst_3 : Field E'
inst_4 : Algebra F E'
h : ∀ (x : E), IsIntegral F x ∧ Splits (map (algebraMap F E) (minpoly F x))
f : E ≃ₐ[F] E'
x : E'
⊢ IsIntegral F x ∧ Splits (map (algebraMap F E') (minpoly F x))
have h₁ : IsIntegral.{u_1, u_3} F (A := E) ((f.symm : (a : E') → E) x : E) ∧
  Splits (map (algebraMap F E) (minpoly.{u_1, u_3} F (B := E) ((f.symm : (a : E') → E) x : E)))
Tactic: specialize h (f.symm x)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
E' : Type u_4
inst_3 : Field E'
inst_4 : Algebra F E'
f : E ≃ₐ[F] E'
x : E'
h :
  IsIntegral.{u_1, u_3} F (A := E) ((f.symm : (a : E') → E) x : E) ∧
    Splits (map (algebraMap F E) (minpoly.{u_1, u_3} F (B := E) ((f.symm : (a : E') → E) x : E)))
⊢ IsIntegral F x ∧ Splits (map (algebraMap F E') (minpoly F x))
have rw : IsIntegral.{u_1, u_4} F (A := E') ((f : (a : E) → E') ((f.symm : (a : E') → E) x : E) : E') ∧
  Splits
    (map (↑(↑f : E →ₐ[F] E') : E →+* E')
      (map (algebraMap F E) (minpoly.{u_1, u_3} F (B := E) ((f.symm : (a : E') → E) x : E))))
Tactic: rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap, ← map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
M : Type u_5
N : Type u_6
inst_3 : Field N
inst_4 : Field M
inst_5 : Algebra M N
inst_6 : Algebra.IsAlgebraic F E
h : Normal F E
f : F ≃+* M
g : E ≃+* N
hcomp :
  Eq (α := F →+* N) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap M N) (↑f : F →+* M))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : E →+* N) (algebraMap F E))
⊢ Normal M N
have rw : ∀ (h : ∀ (x : E), IsIntegral F x ∧ Splits (map (algebraMap F E) (minpoly F x))) {f : F ≃+* M} {g : E ≃+* N}
  (hcomp :
    Eq (α := F →+* N) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap M N) (↑f : F →+* M))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : E →+* N) (algebraMap F E)))
  (x : N), IsIntegral M x ∧ Splits (map (algebraMap M N) (minpoly M x))
Tactic: rw [normal_iff] at h ⊢
Cleared hypotheses: h, f, g, hcomp
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
M : Type u_5
N : Type u_6
inst_3 : Field N
inst_4 : Field M
inst_5 : Algebra M N
inst_6 : Algebra.IsAlgebraic F E
h : ∀ (x : E), IsIntegral F x ∧ Splits (map (algebraMap F E) (minpoly F x))
f : F ≃+* M
g : E ≃+* N
hcomp :
  Eq (α := F →+* N) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap M N) (↑f : F →+* M))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : E →+* N) (algebraMap F E))
x : N
⊢ IsIntegral M x ∧ Splits (map (algebraMap M N) (minpoly M x))
have rw : IsIntegral.{u_5, u_6} M (A := N) ((g : (a : E) → N) ((g.symm : (a : N) → E) x : E) : N) ∧
  Splits (map (algebraMap M N) (minpoly.{u_5, u_6} M (B := N) ((g : (a : E) → N) ((g.symm : (a : N) → E) x : E) : N)))
Tactic: rw [← g.apply_symm_apply x]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
M : Type u_5
N : Type u_6
inst_3 : Field N
inst_4 : Field M
inst_5 : Algebra M N
inst_6 : Algebra.IsAlgebraic F E
h : ∀ (x : E), IsIntegral F x ∧ Splits (map (algebraMap F E) (minpoly F x))
f : F ≃+* M
g : E ≃+* N
hcomp :
  Eq (α := F →+* N) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap M N) (↑f : F →+* M))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : E →+* N) (algebraMap F E))
x : N
⊢ Splits (map (algebraMap M N) (minpoly.{u_5, u_6} M (B := N) ((g : (a : E) → N) ((g.symm : (a : N) → E) x : E) : N)))
have rw : Splits (map (↑g : E →+* N) (map (algebraMap F E) (minpoly.{u_1, u_3} F (B := E) ((g.symm : (a : N) → E) x : E))))
Tactic: rw [← minpoly.map_eq_of_equiv_equiv hcomp, map_map, hcomp, ← map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
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 K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x : ↥(AlgHom.range (toAlgHom F E K₁))
⊢ Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) ((ϕ : (a : K₁) → K₂) (↑x : K₁) : K₂)
have suffices : Subalgebra.map ϕ (AlgHom.range (toAlgHom F E K₁)) ≤ AlgHom.range (toAlgHom F E K₂)
Tactic: suffices (toAlgHom F E K₁).range.map ϕ ≤ _ by exact this ⟨x, Subtype.mem x, rfl⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
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 K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ Membership.mem (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) x
have rw : Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂))
  (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)
Tactic: rw [← hx, ← hy]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
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 K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂))
    (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)
have hx₁ : degree
    (minpoly.{u_6, u_4} E (B := K₂)
      (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)) =
  1
Tactic: apply minpoly.mem_range_of_degree_eq_one E
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
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 K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ degree
      (minpoly.{u_6, u_4} E (B := K₂)
        (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)) =
    1
have hx₁ : IsIntegral.{u_6, u_4} E (A := K₂)
  (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)
Tactic: refine ((h.splits z).of_dvd (map_ne_zero (minpoly.ne_zero (h.isIntegral z)))
        (minpoly.dvd E _ (by simp [aeval_algHom_apply]))).degree_eq_one_of_irreducible
        (minpoly.irreducible ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
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 K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ IsIntegral.{u_6, u_4} E (A := K₂)
    (((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) ((toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z : K₁) : K₂)
have hx₁ : IsIntegral.{u_6, u_4} E (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)
Tactic: simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
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 K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
h : Normal F E
x_1 : ↥(AlgHom.range (toAlgHom F E K₁))
x : K₂
y : K₁
hx : ((↑ϕ : K₁ →+* K₂) : (a : K₁) → K₂) y = x
z : E
hy : (toRingHom (toAlgHom F E K₁) : (a : E) → K₁) z = y
⊢ IsIntegral.{u_6, u_4} E (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)
have hx₁ : IsIntegral.{u_1, u_4} F (A := K₂) ((ϕ : (a : K₁) → K₂) ((toAlgHom F E K₁ : (a : E) → K₁) z : K₁) : K₂)
Tactic: suffices IsIntegral F _ by exact this.tower_top
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
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 K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : E →ₐ[F] K₁
⊢ (fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁))
      ((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F))) σ) =
    σ
have H : ∀ (x : E),
  Eq.{u_3 + 1} (α := K₁)
    (((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁))
            ((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F))) σ) :
          (a : E) → K₁)
        x :
      K₁)
    ((σ : (a : E) → K₁) x : K₁)
Tactic: ext