awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
base : P ⊥
⊢ P (adjoin F s)
have ih : ∀ (K : IntermediateField F E),
  ∀ x ∈ (p.aroots E).toFinset, P K → P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
Tactic: apply IntermediateField.induction_on_adjoin_finset _ P
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
⊢ P ⊥
have base : ∀
  (key :
    ∀ (h_sep : IsSeparable.{u_1, u_2} F (K := E) 0)
      (h_splits : Polynomial.Splits (Polynomial.map (algebraMap F E) (minpoly.{u_1, u_2} F (B := E) 0))),
      Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = Polynomial.natDegree (minpoly.{u_1, u_2} F (B := E) 0)),
  P ⊥
Tactic: have key := IntermediateField.card_algHom_adjoin_integral F (K := E)
      (show IsIntegral F (0 : E) from isIntegral_zero)
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
key :
  ∀ (h_sep : IsSeparable.{u_1, u_2} F (K := E) 0)
    (h_splits : Polynomial.Splits (Polynomial.map (algebraMap F E) (minpoly.{u_1, u_2} F (B := E) 0))),
    Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = Polynomial.natDegree (minpoly.{u_1, u_2} F (B := E) 0)
⊢ P ⊥
have key₁ : ∀ (h_sep : Polynomial.Separable.{u_1} (R := F) Polynomial.X)
  (h_splits : Polynomial.Splits (Polynomial.map (algebraMap F E) Polynomial.X)), Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = 1
Tactic: rw [IsSeparable, minpoly.zero, Polynomial.natDegree_X] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
key :
  ∀ (h_sep : Polynomial.Separable.{u_1} (R := F) Polynomial.X)
    (h_splits : Polynomial.Splits (Polynomial.map (algebraMap F E) Polynomial.X)), Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = 1
⊢ P ⊥
have key₁ : Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = 1
Tactic: specialize key Polynomial.separable_X (Polynomial.Splits.X.map (algebraMap F E))
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
key : Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = 1
⊢ P ⊥
have key₁ : Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = finrank.{u_1, u_2} F ↥(toSubalgebra ⊥)
Tactic: rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
key : Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = finrank.{u_1, u_2} F ↥(toSubalgebra ⊥)
⊢ P ⊥
have base : Nat.card.{u_2} (↥⊥ →ₐ[F] E) = Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E)
Tactic: refine Eq.trans ?_ key
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
key : Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = finrank.{u_1, u_2} F ↥(toSubalgebra ⊥)
⊢ Nat.card.{u_2} (↥⊥ →ₐ[F] E) = Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E)
have base : (↥⊥ →ₐ[F] E) ≃ (↥F⟮0⟯ →ₐ[F] E)
Tactic: apply Nat.card_congr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
key : Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = finrank.{u_1, u_2} F ↥(toSubalgebra ⊥)
⊢ (↥⊥ →ₐ[F] E) ≃ (↥F⟮0⟯ →ₐ[F] E)
have base : (↥⊥ →ₐ[F] E) ≃ (↥⊥ →ₐ[F] E)
Tactic: rw [IntermediateField.adjoin_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) →ₐ[F] E) =
    finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
have ih : finrank.{u_1, u_2} F ↥(↥K)⟮x⟯ = finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
Tactic: rw [of_separable_splitting_field_aux hp K (Multiset.mem_toFinset.mp hx), hK, finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
⊢ finrank.{u_1, u_2} F ↥(↥K)⟮x⟯ = finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
have ih : finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) = finrank.{u_1, u_2} F ↥(↥K)⟮x⟯
Tactic: symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
⊢ finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) = finrank.{u_1, u_2} F ↥(↥K)⟮x⟯
have ih : ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) ≃ₗ[F] ↥(↥K)⟮x⟯
Tactic: refine LinearEquiv.finrank_eq ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
⊢ [IsGalois F E, Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥, Nat.card.{u_2} Gal(E/F) = finrank F E,
      ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
have tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
Tactic: tfae_have 1 → 2 := fun h ↦ OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ [IsGalois F E, Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥, Nat.card.{u_2} Gal(E/F) = finrank F E,
      ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
have tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
Tactic: tfae_have 1 → 3 := fun _ ↦ card_aut_eq_finrank F E
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ [IsGalois F E, Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥, Nat.card.{u_2} Gal(E/F) = finrank F E,
      ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
have tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
Tactic: tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ [IsGalois F E, Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥, Nat.card.{u_2} Gal(E/F) = finrank F E,
      ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
have tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
Tactic: tfae_have 2 → 1 := of_fixedField_eq_bot F E
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
⊢ [IsGalois F E, Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥, Nat.card.{u_2} Gal(E/F) = finrank F E,
      ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
have tfae_3_to_1 : ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E
Tactic: tfae_have 3 → 1 := of_card_aut_eq_finrank F E
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
tfae_3_to_1 : ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E
⊢ [IsGalois F E, Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥, Nat.card.{u_2} Gal(E/F) = finrank F E,
      ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
have tfae_4_to_1 : ∀ (a : ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p), IsGalois F E
Tactic: tfae_have 4 → 1 := fun ⟨h, hp1, _⟩ ↦ of_separable_splitting_field hp1
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
⊢ IsGalois (↥L) E
have obtain : ∀ (T : F[X]) (hT₁ : T.Separable) (hT₂ : Polynomial.IsSplittingField.{u_1, u_2} F (↥K) T), IsGalois (↥L) E
Tactic: obtain ⟨T, hT₁, hT₂⟩ := IsGalois.is_separable_splitting_field F K
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : Polynomial.IsSplittingField.{u_1, u_2} F (↥K) T
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ IsGalois (↥L) E
have suffices : Polynomial.IsSplittingField (↥L) E T'
Tactic: suffices T'.IsSplittingField L E from IsGalois.of_separable_splitting_field (p := T') hT₁.map
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : Polynomial.IsSplittingField.{u_1, u_2} F (↥K) T
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Polynomial.IsSplittingField (↥L) E T'
have rw : ∀
  (hT₂ :
    Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
      Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤),
  let T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T;
  Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T') ∧
    Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
Tactic: rw [isSplittingField_iff_intermediateField] at hT₂ ⊢
Cleared hypotheses: hT₂, T'
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T') ∧
    Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have left : Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T')
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
left : Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T')
⊢ Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T') ∧
    Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right : Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T')
have left : Polynomial.Splits (Polynomial.map (algebraMap F E) T)
Tactic: rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have h' : T'.rootSet E = T.rootSet E
Tactic: have h' : T'.rootSet E = T.rootSet E := by simp [Set.ext_iff, Polynomial.mem_rootSet', T']
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right : ∀
  (hT₂ :
    Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
      Eq (α := IntermediateField F E) (adjoin F (T.rootSet E)) (lift (F := K) ⊤)),
  let T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T;
  ∀ (h' : T'.rootSet E = T.rootSet E), Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
Tactic: rw [← lift_inj, lift_adjoin, ← coe_val, hT₂.1.image_rootSet] at hT₂
Cleared hypotheses: hT₂, T', h'
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq (α := IntermediateField F E) (adjoin F (T.rootSet E)) (lift (F := K) ⊤)
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right : Eq (α := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (adjoin (↥L) (T'.rootSet E))) ⊤
Tactic: rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq (α := IntermediateField F E) (adjoin F (T.rootSet E)) (lift (F := K) ⊤)
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
right : Eq (α := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (adjoin (↥L) (T'.rootSet E))) ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right₁ : Eq (α := IntermediateField F E) (adjoin F ((↑L : Set E) ∪ T'.rootSet E)) ⊤
Tactic: rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq (α := IntermediateField F E) (adjoin F (T.rootSet E)) (lift (F := K) ⊤)
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
right : Eq (α := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (adjoin (↥L) (T'.rootSet E))) ⊤
right₁ : Eq (α := IntermediateField F E) (adjoin F ((↑L : Set E) ∪ T'.rootSet E)) ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right₂ : Eq (α := IntermediateField F E) (adjoin F (↑L : Set E) ⊔ adjoin F (T'.rootSet E)) ⊤
Tactic: rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq (α := IntermediateField F E) (adjoin F (T.rootSet E)) (lift (F := K) ⊤)
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
right : Eq (α := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (adjoin (↥L) (T'.rootSet E))) ⊤
right₁ : Eq (α := IntermediateField F E) (adjoin F ((↑L : Set E) ∪ T'.rootSet E)) ⊤
right₂ : Eq (α := IntermediateField F E) (adjoin F (↑L : Set E) ⊔ adjoin F (T'.rootSet E)) ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right₃ : L ⊔ adjoin F (T'.rootSet E) = ⊤
Tactic: rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]