awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Basic
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
rw : ∑ a : K →ₐ[F] E, Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (K →ₐ[F] E) * Polynomial.natDegree (minpoly 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⟯

Tactic:
rw [Nat.card_congr key_equiv, Nat.card_sigma, IntermediateField.adjoin.finrank h,
    Nat.card_eq_fintype_card]

Premises used: IntermediateField.adjoin.finrank, Nat.card_congr, Nat.card_sigma, Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Galois.Basic
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
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)
⊢ ∑ a : K →ₐ[F] E, Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (K →ₐ[F] E) * Polynomial.natDegree (minpoly K x)

Tactic:
apply Finset.sum_const_nat

Premises used: Finset.sum_const_nat
-- Module: Mathlib.FieldTheory.Galois.Basic
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₁ :
  Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f →
    Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Polynomial.natDegree (minpoly K x)
⊢ Membership.mem (γ := Finset (K →ₐ[F] E)) Finset.univ f →
    Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Polynomial.natDegree (minpoly K x)

Tactic:
_
-- Module: Mathlib.FieldTheory.Galois.Basic
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
h₂ : Polynomial.Splits (Polynomial.map (algebraMap K E) (minpoly K x))
⊢ Nat.card.{u_2} (↥K⟮x⟯ →ₐ[K] E) = Polynomial.natDegree (minpoly K x)

Tactic:
rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) h]

Premises used: IntermediateField.card_algHom_adjoin_integral
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ IsSeparable K x

Tactic:
Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2

Premises used: Iff.mpr, Algebra.algebraMap, IsSeparable, Polynomial.Separable.of_dvd, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ IsSeparable K x

Tactic:
exact Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2

Premises used: Iff.mpr, Algebra.algebraMap, Polynomial.Separable.of_dvd, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.Galois.Basic
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 (algebraMap F E) p)
⊢ Polynomial.Splits (Polynomial.map (algebraMap K E) (minpoly K x))

Tactic:
apply sp.splits.of_dvd (Polynomial.map_ne_zero h1)

Premises used: Polynomial.IsSplittingField.splits, Polynomial.Splits.of_dvd, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
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))
h₃ :
  Dvd.dvd (α := E[X]) (Polynomial.map (↑f : K →+* E) (minpoly K x))
    (Polynomial.map (↑f : K →+* E) (Polynomial.map (algebraMap F K) p))
h₄ h₅ h₆ h₇ : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
⊢ Dvd.dvd (α := E[X]) (Polynomial.map (algebraMap K E) (minpoly K x)) (Polynomial.map (algebraMap F E) p)

Tactic:
rwa [← f.comp_algebraMap, ← p.map_map, RingHom.algebraMap_toAlgebra, Polynomial.map_dvd_map']

Premises used: AlgHom.comp_algebraMap, RingHom.algebraMap_toAlgebra, Polynomial.map_map, Polynomial.map_dvd_map'
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ FiniteDimensional F E

Tactic:
haveI hFE : FiniteDimensional F E := Polynomial.IsSplittingField.finiteDimensional E p
-- Module: Mathlib.FieldTheory.Galois.Basic
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
a : Eq (α := Subalgebra F E) (toSubalgebra (adjoin F s)) (toSubalgebra ⊤)
⊢ Eq (α := IntermediateField F E) (adjoin F s) ⊤

Tactic:
apply IntermediateField.toSubalgebra_injective

Premises used: IntermediateField.toSubalgebra_injective
-- Module: Mathlib.FieldTheory.Galois.Basic
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
a : LE.le (α := Subalgebra F E) (Algebra.adjoin F (p.rootSet E)) (toSubalgebra (adjoin F s))
⊢ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F s)) (toSubalgebra ⊤)

Tactic:
rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]

Premises used: Polynomial.IsSplittingField.adjoin_rootSet, IntermediateField.top_toSubalgebra, top_le_iff
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ LE.le (α := Subalgebra F E) (Algebra.adjoin F (p.rootSet E)) (toSubalgebra (adjoin F s))

Tactic:
apply IntermediateField.algebra_adjoin_le_adjoin

Premises used: IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.Galois.Basic
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) ⊤

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
-- Module: Mathlib.FieldTheory.Galois.Basic
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)
⊢ P ⊤

Tactic:
rw [adjoin_root] at this
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ⊤
h : Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ IsGalois F E

Tactic:
apply of_card_aut_eq_finrank

Premises used: IsGalois.of_card_aut_eq_finrank
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ⊤
h : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} (↥⊤ →ₐ[F] E)
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E

Tactic:
rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]

Premises used: LinearEquiv.finrank_eq, AlgEquiv.toLinearEquiv, IntermediateField.topEquiv, Eq.trans
-- Module: Mathlib.FieldTheory.Galois.Basic
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) = Nat.card.{u_2} (↥⊤ →ₐ[F] E)

Tactic:
Nat.card_congr ((algEquivEquivAlgHom F E).toEquiv.trans
      (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))

Premises used: AlgEquiv.symm, Equiv.trans, MulEquiv.toEquiv, algEquivEquivAlgHom, Nat.card_congr, AlgEquiv.arrowCongr, AlgEquiv.refl, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
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) = Nat.card.{u_2} (↥⊤ →ₐ[F] E)

Tactic:
exact Nat.card_congr ((algEquivEquivAlgHom F E).toEquiv.trans
      (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))

Premises used: AlgEquiv.symm, Equiv.trans, MulEquiv.toEquiv, algEquivEquivAlgHom, Nat.card_congr, AlgEquiv.arrowCongr, AlgEquiv.refl, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
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
suffices : P (adjoin F s)
⊢ IsGalois F E

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))
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ⊥
ih :
  ∀ (K : IntermediateField F E),
    ∀ x ∈ (p.aroots E).toFinset, P K → P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ P (adjoin F s)

Tactic:
apply IntermediateField.induction_on_adjoin_finset _ P

Premises used: IntermediateField.induction_on_adjoin_finset
-- Module: Mathlib.FieldTheory.Galois.Basic
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 :
  ∀
    (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 ⊥
⊢ P ⊥

Tactic:
have key := IntermediateField.card_algHom_adjoin_integral F (K := E)
      (show IsIntegral F (0 : E) from isIntegral_zero)
-- Module: Mathlib.FieldTheory.Galois.Basic
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)
⊢ ∀ (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

Premises used: Polynomial.natDegree_X, minpoly.zero, IsSeparable
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E) = 1

Tactic:
specialize key Polynomial.separable_X (Polynomial.Splits.X.map (algebraMap F E))

Premises used: Algebra.algebraMap, Polynomial.separable_X, Polynomial.Splits.X, Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ 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

Premises used: IntermediateField.bot_toSubalgebra, Subalgebra.finrank_bot
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ⊥

Tactic:
Eq.trans ?_ key

Premises used: Eq.trans
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ⊥)
base : Nat.card.{u_2} (↥⊥ →ₐ[F] E) = Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E)
⊢ P ⊥

Tactic:
refine Eq.trans ?_ key

Premises used: Eq.trans
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ⊥)
base : (↥⊥ →ₐ[F] E) ≃ (↥F⟮0⟯ →ₐ[F] E)
⊢ Nat.card.{u_2} (↥⊥ →ₐ[F] E) = Nat.card.{u_2} (↥F⟮0⟯ →ₐ[F] E)

Tactic:
apply Nat.card_congr

Premises used: Nat.card_congr
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ⊥)
base base₁ : (↥⊥ →ₐ[F] E) ≃ (↥⊥ →ₐ[F] E)
⊢ (↥⊥ →ₐ[F] E) ≃ (↥F⟮0⟯ →ₐ[F] E)

Tactic:
rw [IntermediateField.adjoin_zero]

Premises used: IntermediateField.adjoin_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
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 : P K
ih :
  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⟯)
⊢ P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)

Tactic:
simp only [P] at *