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
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
h₂ : finrank.{u_1, u_2} F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E
h₃ : finrank F E = 1 * finrank (↥(fixedField ⊤)) E
h₄ : Nat.card.{u_2} Gal(E/F) = 1 * finrank (↥(fixedField ⊤)) E
h₅ : Nat.card.{u_2} Gal(E/F) = finrank (↥(fixedField ⊤)) E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₆ : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} ↥⊤
Tactic: classical
  rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
    finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]
  apply Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
-- 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
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
h₂ : finrank.{u_1, u_2} F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E
h₃ : finrank F E = 1 * finrank (↥(fixedField ⊤)) E
h₄ : Nat.card.{u_2} Gal(E/F) = 1 * finrank (↥(fixedField ⊤)) E
h₅ : Nat.card.{u_2} Gal(E/F) = finrank (↥(fixedField ⊤)) E
h₆ h₇ h₈ : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} ↥⊤
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₉ : Gal(E/F) ≃ ↥⊤
Tactic: classical
  rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
    finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]
  apply Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) =
    Nat.card (K →ₐ[F] E) * finrank.{u_3, u_2} K ↥K⟮x⟯
have h : IsIntegral K x
Tactic: have h : IsIntegral K x := (isIntegral_of_noetherian (IsNoetherian.iff_fg.2 hFE) x).tower_top
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp_1 : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
hp : p = 0
⊢ False
have hx₁ : Membership.mem (γ := Multiset E) 0 x
Tactic: rw [hp, Polynomial.aroots_zero] at hx
Cleared hypotheses: hx, h, hp
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) =
    Nat.card (K →ₐ[F] E) * finrank.{u_3, u_2} K ↥K⟮x⟯
have h1 : p ≠ 0
Tactic: have h1 : p ≠ 0 := fun hp => by
    rw [hp, Polynomial.aroots_zero] at hx
    exact Multiset.notMem_zero x hx
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
have hp₁ : Eq.{u_2 + 1} (α := E) ((Polynomial.aeval x : (a : K[X]) → E) (Polynomial.map (algebraMap F K) p) : E) (0 : E)
Tactic: apply minpoly.dvd
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Eq.{u_2 + 1} (α := E) ((Polynomial.aeval x : (a : K[X]) → E) (Polynomial.map (algebraMap F K) p) : E) (0 : E)
have hp₁ : Polynomial.eval x (Polynomial.map (algebraMap F E) p) = 0
Tactic: rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) =
    Nat.card (K →ₐ[F] E) * finrank.{u_3, u_2} K ↥K⟮x⟯
have h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
Tactic: have h2 : minpoly K x ∣ p.map (algebraMap F K) := by
    apply minpoly.dvd
    rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ←
      IsScalarTower.algebraMap_eq]
    exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
⊢ (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)
have change : (↥K⟮x⟯ →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)
Tactic: change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
f : K →ₐ[F] E
⊢ Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
have this : Finite ((f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E))
Tactic: have := Finite.of_equiv _ key_equiv
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) =
    Nat.card (K →ₐ[F] E) * finrank.{u_3, u_2} K ↥K⟮x⟯
have this : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
Tactic: haveI : ∀ f : K →ₐ[F] E, Finite (@AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f)) := fun f => by
    have := Finite.of_equiv _ key_equiv
    apply Finite.of_injective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) =
    Nat.card (K →ₐ[F] E) * finrank.{u_3, u_2} K ↥K⟮x⟯
have this₁ : FiniteDimensional F K
Tactic: have : FiniteDimensional F K := FiniteDimensional.left F K E
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) =
    Nat.card (K →ₐ[F] E) * finrank.{u_3, u_2} K ↥K⟮x⟯
have rw : ∑ a : K →ₐ[F] E, Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (K →ₐ[F] E) * Polynomial.natDegree (minpoly K x)
Tactic: rw [Nat.card_congr key_equiv, Nat.card_sigma, IntermediateField.adjoin.finrank h,
    Nat.card_eq_fintype_card]
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
⊢ ∑ a : K →ₐ[F] E, Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (K →ₐ[F] E) * Polynomial.natDegree (minpoly K x)
have h₁ : ∀ (x_1 : K →ₐ[F] E),
  Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ x_1 →
    Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Polynomial.natDegree (minpoly K x)
Tactic: apply Finset.sum_const_nat
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
h_1 : Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f
⊢ Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Polynomial.natDegree (minpoly K x)
have h₁ : IsSeparable K x
Tactic: rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) 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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
h_1 : Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f
h₁ : IsSeparable K x
⊢ Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Polynomial.natDegree (minpoly K x)
have h₂ : Polynomial.Splits (Polynomial.map (algebraMap K E) (minpoly K x))
Tactic: rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) 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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
h_1 : Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f
⊢ Polynomial.Splits (Polynomial.map (algebraMap K E) (minpoly K x))
have h₁ : Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x)) (Polynomial.map (algebraMap F E) p)
Tactic: apply sp.splits.of_dvd (Polynomial.map_ne_zero h1)
-- 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]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
h_1 : Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f
⊢ Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x)) (Polynomial.map (algebraMap F E) p)
have h₁ : Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x))
  (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* E) (algebraMap F K)) p)
Tactic: rwa [← f.comp_algebraMap, ← p.map_map, RingHom.algebraMap_toAlgebra, Polynomial.map_dvd_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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
h_1 : Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f
h₁ :
  Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x))
    (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* E) (algebraMap F K)) p)
⊢ Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x)) (Polynomial.map (algebraMap F E) p)
have h₂ : Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x))
  (Polynomial.map (↑f : K →+* E) (Polynomial.map (algebraMap F K) p))
Tactic: rwa [← f.comp_algebraMap, ← p.map_map, RingHom.algebraMap_toAlgebra, Polynomial.map_dvd_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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this_1 : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
h_1 : Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f
h₁ :
  Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x))
    (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* E) (algebraMap F K)) p)
h₂ :
  Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x))
    (Polynomial.map (↑f : K →+* E) (Polynomial.map (algebraMap F K) p))
⊢ Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x)) (Polynomial.map (algebraMap F E) p)
have h₃ : Dvd.dvd (α := E[X]) (Polynomial.map (↑f : K →+* E) (minpoly K x))
  (Polynomial.map (↑f : K →+* E) (Polynomial.map (algebraMap F K) p))
Tactic: rwa [← f.comp_algebraMap, ← p.map_map, RingHom.algebraMap_toAlgebra, Polynomial.map_dvd_map']
-- 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
⊢ IsGalois F E
have hFE : FiniteDimensional F E
Tactic: haveI hFE : FiniteDimensional F E := Polynomial.IsSplittingField.finiteDimensional E 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
⊢ Eq (α := IntermediateField F E) (adjoin F s) ⊤
have a : Eq (α := Subalgebra F E) (toSubalgebra (adjoin F s)) (toSubalgebra ⊤)
Tactic: apply IntermediateField.toSubalgebra_injective
-- 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
⊢ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F s)) (toSubalgebra ⊤)
have a : LE.le (α := Subalgebra F E) (Algebra.adjoin F (p.rootSet E)) (toSubalgebra (adjoin F s))
Tactic: rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]
-- 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
⊢ IsGalois F E
have adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
Tactic: have adjoin_root : IntermediateField.adjoin F s = ⊤ := by
    apply IntermediateField.toSubalgebra_injective
    rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]
    apply IntermediateField.algebra_adjoin_le_adjoin
-- 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_1 : 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
this : P (adjoin F s)
⊢ IsGalois F E
have this₁ : P ⊤
Tactic: rw [adjoin_root] at this
Cleared hypotheses: this
-- 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_1 : 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
this : P ⊤
⊢ IsGalois F E
have h : Nat.card.{u_2} Gal(E/F) = finrank F E
Tactic: apply of_card_aut_eq_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_1 : 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
this : P ⊤
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E
have h : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} (↥⊤ →ₐ[F] E)
Tactic: rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]
-- 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
⊢ IsGalois F E
have suffices : P (adjoin F s)
Tactic: suffices P (IntermediateField.adjoin F s) by
    rw [adjoin_root] at this
    apply of_card_aut_eq_finrank
    rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]
    exact Nat.card_congr ((algEquivEquivAlgHom F E).toEquiv.trans
      (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))
-- 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 (adjoin F s)
have base : P ⊥
Tactic: apply IntermediateField.induction_on_adjoin_finset _ P