awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Normal.Closure
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

Tactic:
⟨@AlgHom.fieldRange_of_normal (E := K), normal_iff_forall_fieldRange_le.2 ∘ fun h σ ↦ (h σ).le⟩

Premises used: Iff.mpr, Function.comp, IntermediateField.normal_iff_forall_fieldRange_le, Eq.le, Iff.intro, AlgHom.fieldRange_of_normal
-- Module: Mathlib.FieldTheory.Normal.Closure
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

Tactic:
⟨fun h σ ↦ (K.fieldRange_val ▸ AlgHom.map_fieldRange K.val σ).trans
  (normal_iff_forall_fieldRange_eq.1 h _), fun h ↦ normal_iff_forall_map_le.2 (fun σ ↦ (h σ).le)⟩

Premises used: Iff.mpr, Eq.le, IntermediateField.normal_iff_forall_map_le, Iff.intro
-- Module: Mathlib.FieldTheory.Normal.Closure
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

Tactic:
⟨fun h σ ↦ normal_iff_forall_map_eq.1 h σ, fun h ↦ normal_iff_forall_map_le'.2 (fun σ ↦ (h σ).le)⟩

Premises used: Iff.mpr, IntermediateField.normal_iff_forall_map_eq, AlgEquiv.toAlgHom, Eq.le, IntermediateField.normal_iff_forall_map_le', Iff.intro, Iff.mp
-- Module: Mathlib.FieldTheory.Normal.Closure
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)
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)
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥(map (↑σ : L →ₐ[F] L) K)) L) (normalClosure F (↥K) L)

Tactic:
simp_rw [normalClosure_def'', map_map]

Premises used: IntermediateField.map_map, IntermediateField.normalClosure_def''
-- Module: Mathlib.FieldTheory.Normal.Closure
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.{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:
(Equiv.mulRight σ).iSup_congr fun _ ↦ rfl

Premises used: Equiv.mulRight, Equiv.iSup_congr, rfl
-- Module: Mathlib.FieldTheory.Normal.Closure
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.{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:
exact (Equiv.mulRight σ).iSup_congr fun _ ↦ rfl

Premises used: Equiv.mulRight, Equiv.iSup_congr, rfl
-- Module: Mathlib.FieldTheory.Normal.Closure
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
⊢ ∀ (σ : 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
-- Module: Mathlib.FieldTheory.Normal.Closure
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
this :
  ∀ (σ : Gal(L/F)),
    Eq (α := IntermediateField F L) (normalClosure F (↥(map (↑σ : L →ₐ[F] L) K)) L) (normalClosure F (↥K) L)
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥(map σ K)) L) (normalClosure F (↥K) L)

Tactic:
this ((Algebra.IsAlgebraic.algEquivEquivAlgHom _ _).symm σ)

Premises used: AlgEquiv.toAlgHom, Set.Mem, MulEquiv.symm, Algebra.IsAlgebraic.algEquivEquivAlgHom, DFunLike.coe
-- Module: Mathlib.FieldTheory.Normal.Closure
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
this :
  ∀ (σ : Gal(L/F)),
    Eq (α := IntermediateField F L) (normalClosure F (↥(map (↑σ : L →ₐ[F] L) K)) L) (normalClosure F (↥K) L)
⊢ Eq (α := IntermediateField F L) (normalClosure F (↥(map σ K)) L) (normalClosure F (↥K) L)

Tactic:
exact this ((Algebra.IsAlgebraic.algEquivEquivAlgHom _ _).symm σ)

Premises used: MulEquiv.symm, Algebra.IsAlgebraic.algEquivEquivAlgHom, DFunLike.coe
-- Module: Mathlib.FieldTheory.Normal.Closure
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₂

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

Premises used: Iff.intro
-- Module: Mathlib.FieldTheory.Normal.Closure
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₂
refine_2 : ∀ (h : K₁ ≤ K₂), normalClosure F (↥K₁) L ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.FieldTheory.Normal.Closure
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₂
⊢ ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂

Tactic:
rw [normalClosure_le_iff] at h

Premises used: normalClosure_le_iff
-- Module: Mathlib.FieldTheory.Normal.Closure
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 : ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂
⊢ K₁ ≤ K₂

Tactic:
simpa only [fieldRange_val] using h K₁.val

Premises used: IntermediateField.val, IntermediateField.fieldRange_val
-- Module: Mathlib.FieldTheory.Normal.Closure
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₂
refine_2 : LE.le (α := IntermediateField F L) (normalClosure F (↥K₁) L) (normalClosure F (↥K₂) L)
⊢ normalClosure F (↥K₁) L ≤ K₂

Tactic:
rw [← normalClosure_of_normal K₂]

Premises used: IntermediateField.normalClosure_of_normal
-- Module: Mathlib.FieldTheory.Normal.Closure
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₂
⊢ LE.le (α := IntermediateField F L) (normalClosure F (↥K₁) L) (normalClosure F (↥K₂) L)

Tactic:
normalClosure_mono K₁ K₂ h

Premises used: IntermediateField.normalClosure_mono
-- Module: Mathlib.FieldTheory.Normal.Closure
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₂
⊢ LE.le (α := IntermediateField F L) (normalClosure F (↥K₁) L) (normalClosure F (↥K₂) L)

Tactic:
exact normalClosure_mono K₁ K₂ h

Premises used: IntermediateField.normalClosure_mono
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
x : K
⊢ IsIntegral F x

Tactic:
Algebra.IsIntegral.isIntegral x

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
x : K
⊢ Splits (map (algebraMap F K) (minpoly F x))

Tactic:
Normal.splits' x

Premises used: Normal.splits'
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
⊢ Normal F K ↔ ∀ (x : K), IsIntegral F x ∧ Splits (map (algebraMap F K) (minpoly F x))

Tactic:
⟨fun h x => ⟨h.isIntegral x, h.splits x⟩, fun h =>
    { isAlgebraic := fun x => (h x).1.isAlgebraic
      splits' := fun x => (h x).2 }⟩

Premises used: Normal.mk, Normal.splits, Normal.isIntegral, And.right, And.intro, Iff.intro
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
⊢ Normal F K → ∀ (x : K), IsIntegral F x ∧ Splits (map (algebraMap F K) (minpoly F x))

Tactic:
normal_iff.1

Premises used: normal_iff, Iff.mp
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
x : F
⊢ Splits (map (algebraMap F F) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])))

Tactic:
simp
-- Module: Mathlib.FieldTheory.Normal.Defs
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 F x

Tactic:
obtain ⟨hx, hhx⟩ := h.out x

Premises used: Normal.out
-- Module: Mathlib.FieldTheory.Normal.Defs
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
⊢ Splits (map (algebraMap F E) (minpoly F x))

Tactic:
obtain ⟨hx, hhx⟩ := h.out x

Premises used: Normal.out
-- Module: Mathlib.FieldTheory.Normal.Defs
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))
⊢ Splits (map (algebraMap K E) (map (algebraMap F K) (minpoly F x)))

Tactic:
rw [algebraMap_eq F K E, ← map_map] at hhx

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Normal.Defs
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 K E) (map (algebraMap F K) (minpoly F x)))
⊢ IsIntegral K x ∧ Splits (map (algebraMap K E) (minpoly K x))

Tactic:
⟨hx.tower_top, hhx.of_dvd (map_ne_zero (map_ne_zero (minpoly.ne_zero hx)))
      ((map_dvd_map' _).mpr (minpoly.dvd_map_of_isScalarTower F K x))⟩

Premises used: Iff.mpr, minpoly.dvd_map_of_isScalarTower, And.intro, Polynomial.Splits.of_dvd, IsIntegral.tower_top, Polynomial.map_ne_zero, Polynomial.map_dvd_map', minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Defs
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 K E) (map (algebraMap F K) (minpoly F x)))
⊢ IsIntegral K x ∧ Splits (map (algebraMap K E) (minpoly K x))

Tactic:
exact ⟨hx.tower_top, hhx.of_dvd (map_ne_zero (map_ne_zero (minpoly.ne_zero hx)))
      ((map_dvd_map' _).mpr (minpoly.dvd_map_of_isScalarTower F K x))⟩
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K_1 : Type u_2
inst : Field F
inst_1 : Field K_1
inst_2 : Algebra F K_1
E : Type u_3
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K_1 E
inst_6 : IsScalarTower F K_1 E
K : IntermediateField F E
inst_7 : Normal F E
⊢ Normal (↥K) E

Tactic:
Normal.tower_top_of_normal F K E

Premises used: Membership.mem, Subtype, Normal.tower_top_of_normal
-- Module: Mathlib.FieldTheory.Normal.Defs
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
ϕ : E →ₐ[F] K
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := E) (β := K) (⇑ϕ : (a : E) → K)

Tactic:
h.toIsAlgebraic.bijective_of_isScalarTower' ϕ

Premises used: Algebra.IsAlgebraic.bijective_of_isScalarTower'
-- Module: Mathlib.FieldTheory.Normal.Defs
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'
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))
⊢ Normal F E'

Tactic:
rw [normal_iff] at h ⊢

Premises used: normal_iff
-- Module: Mathlib.FieldTheory.Normal.Defs
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.{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)

Premises used: AlgEquiv.symm, DFunLike.coe
-- Module: Mathlib.FieldTheory.Normal.Defs
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)))
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))))
⊢ IsIntegral F x ∧ Splits (map (algebraMap F E') (minpoly F x))

Tactic:
rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap, ← map_map]

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom, minpoly.algEquiv_eq, AlgEquiv.apply_symm_apply, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Normal.Defs
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.{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:
⟨h.1.map f, h.2.map _⟩

Premises used: And.right, IsIntegral.map, And.left, And.intro, Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.Normal.Defs
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.{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:
exact ⟨h.1.map f, h.2.map _⟩
-- Module: Mathlib.FieldTheory.Normal.Defs
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'
⊢ Normal F E ↔ Normal F E'

Tactic:
⟨fun _ ↦ Normal.of_algEquiv f, fun _ ↦ Normal.of_algEquiv f.symm⟩

Premises used: AlgEquiv.symm, Normal.of_algEquiv, Iff.intro
-- Module: Mathlib.FieldTheory.Normal.Defs
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))
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))
⊢ Normal M N

Tactic:
rw [normal_iff] at h ⊢

Premises used: normal_iff
-- Module: Mathlib.FieldTheory.Normal.Defs
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
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)))
⊢ IsIntegral M x ∧ Splits (map (algebraMap M N) (minpoly M x))

Tactic:
rw [← g.apply_symm_apply x]

Premises used: RingEquiv.apply_symm_apply
-- Module: Mathlib.FieldTheory.Normal.Defs
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.{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:
⟨(h (g.symm x)).1.map_of_comp_eq _ _ hcomp, ?_⟩

Premises used: And.left, IsIntegral.map_of_comp_eq, And.intro, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.FieldTheory.Normal.Defs
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
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))))
⊢ 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 [← minpoly.map_eq_of_equiv_equiv hcomp, map_map, hcomp, ← map_map]

Premises used: Polynomial.map_map, minpoly.map_eq_of_equiv_equiv
-- Module: Mathlib.FieldTheory.Normal.Defs
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 (↑g : E →+* N) (map (algebraMap F E) (minpoly.{u_1, u_3} F (B := E) ((g.symm : (a : N) → E) x : E))))

Tactic:
(h (g.symm x)).2.map _

Premises used: And.right, Polynomial.Splits.map, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.FieldTheory.Normal.Defs
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 (↑g : E →+* N) (map (algebraMap F E) (minpoly.{u_1, u_3} F (B := E) ((g.symm : (a : N) → E) x : E))))

Tactic:
exact (h (g.symm x)).2.map _

Premises used: And.right, Polynomial.Splits.map, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.FieldTheory.Normal.Defs
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra K L
inst_6 : IsScalarTower F K L
E : IntermediateField K L
⊢ Normal.{u_1, u_3} F ↥(restrictScalars F E) ↔ Normal.{u_1, u_3} F ↥E

Tactic:
Iff.rfl

Premises used: IntermediateField.restrictScalars, Set.Mem, Iff.rfl, RingHom.codRestrict
-- Module: Mathlib.FieldTheory.Normal.Defs
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₁))
this : Subalgebra.map ϕ (AlgHom.range (toAlgHom F E K₁)) ≤ AlgHom.range (toAlgHom F E K₂)
⊢ Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) ((ϕ : (a : K₁) → K₂) (↑x : K₁) : K₂)

Tactic:
this ⟨x, Subtype.mem x, rfl⟩

Premises used: And.intro, Subtype.mem, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.FieldTheory.Normal.Defs
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₁))
this : Subalgebra.map ϕ (AlgHom.range (toAlgHom F E K₁)) ≤ AlgHom.range (toAlgHom F E K₂)
⊢ Membership.mem (α := K₂) (γ := Subalgebra F K₂) (AlgHom.range (toAlgHom F E K₂)) ((ϕ : (a : K₁) → K₂) (↑x : K₁) : K₂)

Tactic:
exact this ⟨x, Subtype.mem x, rfl⟩

Premises used: And.intro, Subtype.mem, Exists.intro, Subtype.val, rfl