awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this_2 : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
key₂ :
  HSub.hSub (α := (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) (β :=
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])
      (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)
      ((C :
            (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
              (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
          (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g)) :
        (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) =
    minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
this :
  finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
      finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    finrank K Kx
rwa :
  ∀
    (this :
      f.natDegree * finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = finrank K Kx),
    p.natDegree = f.natDegree * g.natDegree
rwa₁ : ∀ (this : f.natDegree * g.natDegree = finrank K Kx), p.natDegree = f.natDegree * g.natDegree
rwa₂ : ∀ (this : f.natDegree * g.natDegree = (powerBasis ⋯).dim), p.natDegree = f.natDegree * g.natDegree
rwa₃ : ∀ (this : f.natDegree * g.natDegree = p.natDegree), p.natDegree = f.natDegree * g.natDegree
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : p.natDegree = f.natDegree * g.natDegree), p.natDegree = f.natDegree * g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree

Tactic:
rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this

Premises used: PowerBasis.finrank, eq_comm, AdjoinRoot.powerBasis_dim, Irreducible.ne_zero, AdjoinRoot.powerBasis
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsAlgebraic K x
h_ev : Eq.{u_2 + 1} (α := L) ((Polynomial.aeval y : (a : K[X]) → L) (minpoly K x) : L) (0 : L)
⊢ Eq (α := K[X]) (minpoly K y) (minpoly K x)

Tactic:
((eq_iff_aeval_minpoly_eq_zero hx.isIntegral).mpr h_ev).symm

Premises used: Iff.mpr, IsAlgebraic.isIntegral, minpoly.eq_iff_aeval_minpoly_eq_zero, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : Eq (α := K[X]) (minpoly K x) (minpoly K y)
⊢ IsAlgebraic K y

Tactic:
have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : Eq (α := K[X]) (minpoly K x) (minpoly K y)
hy : IsAlgebraic K y
⊢ ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯

Tactic:
exact (adjoinRootEquivAdjoin K hx.isIntegral).symm.trans <|
    (AdjoinRoot.algEquivOfEq _ _ _ h_mp).trans (adjoinRootEquivAdjoin K hy.isIntegral)

Premises used: AlgEquiv.symm, AdjoinRoot.algEquivOfEq, IntermediateField.adjoinRootEquivAdjoin, AlgEquiv.trans, IsAlgebraic.isIntegral
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : Eq (α := K[X]) (minpoly K x) (minpoly K y)
hy : IsAlgebraic K y
rw :
  Eq (α := ↥K⟮y⟯)
    (((adjoinRootEquivAdjoin K ⋯).symm.trans
            (AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K ⋯)) :
          (a : ↥K⟮x⟯) → ↥K⟮y⟯)
        (AdjoinSimple.gen K x) :
      ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
rw₁ :
  Eq.{u_2 + 1} (α := ↥K⟮y⟯)
    ((AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K ⋯) :
          (a : AdjoinRoot (minpoly K x)) → ↥K⟮y⟯)
        (((adjoinRootEquivAdjoin K ⋯).symm : (a : ↥K⟮x⟯) → AdjoinRoot (minpoly K x)) (AdjoinSimple.gen K x)) :
      ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
rw₂ :
  Eq.{u_2 + 1} (α := ↥K⟮y⟯)
    ((AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K ⋯) :
          (a : AdjoinRoot (minpoly K x)) → ↥K⟮y⟯)
        (((adjoinRootEquivAdjoin K ⋯).symm : (a : ↥K⟮x⟯) → AdjoinRoot (minpoly K x))
          ((adjoinRootEquivAdjoin K ⋯ : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯) (AdjoinRoot.root (minpoly K x)))) :
      ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
rw₃ :
  Eq.{u_2 + 1} (α := ↥K⟮y⟯)
    ((AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K ⋯) :
          (a : AdjoinRoot (minpoly K x)) → ↥K⟮y⟯)
        (AdjoinRoot.root (minpoly K x)) :
      ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
rw₄ :
  Eq.{u_2 + 1} (α := ↥K⟮y⟯)
    ((adjoinRootEquivAdjoin K ⋯ : (a : AdjoinRoot (minpoly K y)) → ↥K⟮y⟯)
        ((AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp :
            (a : AdjoinRoot (minpoly K x)) → AdjoinRoot (minpoly K y))
          (AdjoinRoot.root (minpoly K x))) :
      ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
rw₅ :
  Eq.{u_2 + 1} (α := ↥K⟮y⟯)
    ((adjoinRootEquivAdjoin K ⋯ : (a : AdjoinRoot (minpoly K y)) → ↥K⟮y⟯) (AdjoinRoot.root (minpoly K y)) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
rw₆ rw₇ : Eq (α := ↥K⟮y⟯) (AdjoinSimple.gen K y) (AdjoinSimple.gen K y)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)

Tactic:
rw [algEquiv, trans_apply, ← adjoinRootEquivAdjoin_apply_root K hx.isIntegral,
    symm_apply_apply, trans_apply, AdjoinRoot.algEquivOfEq_root,
    adjoinRootEquivAdjoin_apply_root K hy.isIntegral]

Premises used: AdjoinRoot.algEquivOfEq_root, IntermediateField.adjoinRootEquivAdjoin_apply_root, AlgEquiv.symm_apply_apply, IsAlgebraic.isIntegral, AlgEquiv.trans_apply, minpoly.algEquiv
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
pb : PowerBasis K L
rw : Eq (α := K[X]) (minpoly K (B := ↥K⟮pb.gen⟯) (AdjoinSimple.gen K pb.gen)) (minpoly K pb.gen)
rw₁ rw₂ : Eq (α := K[X]) (minpoly K pb.gen) (minpoly K pb.gen)
⊢ Eq (α := K[X]) (minpoly K (adjoin.powerBasis ⋯).gen) (minpoly K pb.gen)

Tactic:
rw [adjoin.powerBasis_gen, minpoly_gen]

Premises used: IntermediateField.minpoly_gen, IntermediateField.adjoin.powerBasis_gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
pb : PowerBasis K L
f : K[X]
⊢ Eq (α := L)
    ((pb.equivAdjoinSimple : (a : ↥K⟮pb.gen⟯) → L)
        ((aeval (AdjoinSimple.gen K pb.gen) : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯) :
      L)
    ((aeval pb.gen : (a : K[X]) → L) f : L)

Tactic:
equivOfMinpoly_aeval _ pb _ f

Premises used: IntermediateField.AdjoinSimple.gen, PowerBasis.equivOfMinpoly_aeval
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
pb : PowerBasis K L
⊢ (pb.equivAdjoinSimple : (a : ↥K⟮pb.gen⟯) → L) (AdjoinSimple.gen K pb.gen) = pb.gen

Tactic:
equivOfMinpoly_gen _ pb _

Premises used: IntermediateField.AdjoinSimple.gen, PowerBasis.equivOfMinpoly_gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
pb : PowerBasis K L
f : K[X]
rw :
  Eq (α := ↥K⟮pb.gen⟯)
    ((((adjoin.powerBasis ⋯).equivOfMinpoly pb ⋯).symm : (a : L) → ↥K⟮pb.gen⟯) ((aeval pb.gen : (a : K[X]) → L) f) :
      ↥K⟮pb.gen⟯)
    ((aeval (AdjoinSimple.gen K pb.gen) : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯)
rw₁ :
  Eq (α := ↥K⟮pb.gen⟯)
    ((pb.equivOfMinpoly (adjoin.powerBasis ⋯) ⋯ : (a : L) → ↥K⟮pb.gen⟯) ((aeval pb.gen : (a : K[X]) → L) f) :
      ↥K⟮pb.gen⟯)
    ((aeval (AdjoinSimple.gen K pb.gen) : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯)
rw₂ :
  Eq.{u_2 + 1} (α := ↥K⟮pb.gen⟯) ((aeval (adjoin.powerBasis ⋯).gen : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯)
    ((aeval (AdjoinSimple.gen K pb.gen) : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := ↥K⟮pb.gen⟯) ((aeval (AdjoinSimple.gen K pb.gen) : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯)
    ((aeval (AdjoinSimple.gen K pb.gen) : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯)
⊢ Eq (α := ↥K⟮pb.gen⟯)
    ((pb.equivAdjoinSimple.symm : (a : L) → ↥K⟮pb.gen⟯) ((aeval pb.gen : (a : K[X]) → L) f) : ↥K⟮pb.gen⟯)
    ((aeval (AdjoinSimple.gen K pb.gen) : (a : K[X]) → ↥K⟮pb.gen⟯) f : ↥K⟮pb.gen⟯)

Tactic:
rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_aeval, adjoin.powerBasis_gen]

Premises used: IntermediateField.adjoin.powerBasis_gen, PowerBasis.equivOfMinpoly_aeval, PowerBasis.equivAdjoinSimple, PowerBasis.equivOfMinpoly_symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
pb : PowerBasis K L
rw :
  Eq (α := ↥K⟮pb.gen⟯) ((((adjoin.powerBasis ⋯).equivOfMinpoly pb ⋯).symm : (a : L) → ↥K⟮pb.gen⟯) pb.gen : ↥K⟮pb.gen⟯)
    (AdjoinSimple.gen K pb.gen : ↥K⟮pb.gen⟯)
rw₁ :
  Eq (α := ↥K⟮pb.gen⟯) ((pb.equivOfMinpoly (adjoin.powerBasis ⋯) ⋯ : (a : L) → ↥K⟮pb.gen⟯) pb.gen : ↥K⟮pb.gen⟯)
    (AdjoinSimple.gen K pb.gen : ↥K⟮pb.gen⟯)
rw₂ : (adjoin.powerBasis ⋯).gen = AdjoinSimple.gen K pb.gen
rw₃ rw₄ : Eq (α := ↥K⟮pb.gen⟯) (AdjoinSimple.gen K pb.gen) (AdjoinSimple.gen K pb.gen)
⊢ Eq (α := ↥K⟮pb.gen⟯) ((pb.equivAdjoinSimple.symm : (a : L) → ↥K⟮pb.gen⟯) pb.gen : ↥K⟮pb.gen⟯)
    (AdjoinSimple.gen K pb.gen : ↥K⟮pb.gen⟯)

Tactic:
rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]

Premises used: IntermediateField.adjoin.powerBasis_gen, PowerBasis.equivOfMinpoly_gen, PowerBasis.equivAdjoinSimple, PowerBasis.equivOfMinpoly_symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u
inst : Field F
E : Type v
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
apply :
  Cardinal.lift.{u, v} (max #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ s) : Type v) ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀
⊢ Cardinal.lift.{u, v} #↥(Subfield.closure (Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ s)) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀

Tactic:
apply (Cardinal.lift_le.mpr (Subfield.cardinalMk_closure_le_max _)).trans

Premises used: Iff.mpr, Subfield.cardinalMk_closure_le_max, LE.le.trans, Cardinal.lift_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u
inst : Field F
E : Type v
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
rw :
  Cardinal.lift.{u, v} #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ s) : Type v) ≤
      max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀ ∧
    ℵ₀ ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀
⊢ Cardinal.lift.{u, v} (max #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ s) : Type v) ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀

Tactic:
rw [lift_max, sup_le_iff, lift_aleph0]

Premises used: sup_le_iff, Cardinal.lift_aleph0, Cardinal.lift_max
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u
inst : Field F
E : Type v
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ s) : Type v) ≤
      max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀ ∧
    ℵ₀ ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀

Tactic:
⟨(Cardinal.lift_le.mpr ((mk_union_le _ _).trans <| add_le_max _ _)).trans ?_, le_sup_right⟩

Premises used: Iff.mpr, le_sup_right, And.intro, LE.le.trans, Cardinal.mk_union_le, Cardinal.add_le_max, Cardinal.lift_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u
inst : Field F
E : Type v
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
refine :
  Cardinal.lift.{u, v}
      (max (max #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) : Type v) #(↑s : Type v)) ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀
⊢ Cardinal.lift.{u, v} #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ s) : Type v) ≤
      max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀ ∧
    ℵ₀ ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀

Tactic:
refine ⟨(Cardinal.lift_le.mpr ((mk_union_le _ _).trans <| add_le_max _ _)).trans ?_, le_sup_right⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u
inst : Field F
E : Type v
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
simp_rw :
  max
      (max (Cardinal.lift.{u, v} #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) : Type v))
        (Cardinal.lift.{u, v} #(↑s : Type v)))
      ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀
⊢ Cardinal.lift.{u, v}
      (max (max #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) : Type v) #(↑s : Type v)) ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀

Tactic:
simp_rw [lift_max, lift_aleph0]

Premises used: Cardinal.lift_aleph0, Cardinal.lift_max
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u
inst : Field F
E : Type v
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
grw grw₁ :
  max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀
⊢ max
      (max (Cardinal.lift.{u, v} #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) : Type v))
        (Cardinal.lift.{u, v} #(↑s : Type v)))
      ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀

Tactic:
grw [mk_range_le_lift]

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u
inst : Field F
E : Type u
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
⊢ #↥(adjoin F s) ≤ max (max #F #(↑s : Type u)) ℵ₀

Tactic:
simpa using lift_cardinalMk_adjoin_le F s

Premises used: IntermediateField.lift_cardinalMk_adjoin_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
hS : ∀ (x_1 : L), Membership.mem (γ := Set L) {x, y} x_1 → IsIntegral K x_1
⊢ Algebra.IsAlgebraic.{u_1, u_2} K ↥K⟮x, y⟯

Tactic:
apply IntermediateField.isAlgebraic_adjoin

Premises used: IntermediateField.isAlgebraic_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
⊢ ∀ (x_1 : L), Membership.mem (γ := Set L) {x, y} x_1 → IsIntegral K x_1

Tactic:
simp [hx, hy]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯

Tactic:
have := adjoin.finiteDimensional hx
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯

Tactic:
have := adjoin.finiteDimensional hy
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
rw : FiniteDimensional.{u_1, u_2} K ↥(K⟮x⟯ ⊔ K⟮y⟯)
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮x, y⟯

Tactic:
rw [← Set.singleton_union, adjoin_union]

Premises used: Set.singleton_union, IntermediateField.adjoin_union
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
⊢ FiniteDimensional.{u_1, u_2} K ↥(K⟮x⟯ ⊔ K⟮y⟯)

Tactic:
finiteDimensional_sup K⟮x⟯ K⟮y⟯

Premises used: IntermediateField.adjoin, Singleton.singleton, IntermediateField.finiteDimensional_sup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
⊢ FiniteDimensional.{u_1, u_2} K ↥(K⟮x⟯ ⊔ K⟮y⟯)

Tactic:
exact finiteDimensional_sup K⟮x⟯ K⟮y⟯

Premises used: IntermediateField.adjoin, Singleton.singleton, IntermediateField.finiteDimensional_sup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
⊢ Membership.mem (γ := IntermediateField K L) K⟮x, y⟯ x

Tactic:
subset_adjoin K {x, y} (Set.mem_insert x {y})

Premises used: Insert.insert, IntermediateField.subset_adjoin, Set.mem_insert, Singleton.singleton
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
⊢ Membership.mem (γ := IntermediateField K L) K⟮x, y⟯ y

Tactic:
subset_adjoin K {x, y} (Set.mem_insert_of_mem x (Set.mem_singleton y))

Premises used: Set.mem_singleton, Set.mem_insert_of_mem, Insert.insert, IntermediateField.subset_adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
⊢ (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gen₁ K x y) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
⊢ (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gen₂ K x y) = y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Eq (α := Subfield E) (toSubfield (adjoin F S))
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))

Tactic:
rfl

Premises used: Subfield.closure, Subring.mk', rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
T : IntermediateField F E
⊢ adjoin F S ≤ T ↔ S ⊆ (↑T : Set E)

Tactic:
⟨fun H => le_trans (le_trans Set.subset_union_right Subfield.subset_closure) H, fun H =>
    (@Subfield.closure_le E _ (Set.range (algebraMap F E) ∪ S) T.toSubfield).mpr
      (Set.union_subset (IntermediateField.set_range_subset T) H)⟩

Premises used: Iff.mpr, Subfield.closure_le, Set.subset_union_right, Set.union_subset, Iff.intro, IntermediateField.set_range_subset, Subfield.subset_closure, le_trans
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ GaloisConnection (adjoin F) fun (x : IntermediateField F E) ↦ (↑x : Set E)

Tactic:
fun _ _ =>
  adjoin_le_iff

Premises used: IntermediateField.adjoin_le_iff, GaloisConnection
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
r : F
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring.{u_1, u_2} (R := F) ⊥))))
    (((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) r)⁻¹ : E)

Tactic:
⟨r⁻¹, map_inv₀ _ _⟩

Premises used: Set.Mem, setOf, map_inv₀, Inv.inv, Exists.intro, Set.range
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
r : F
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring.{u_1, u_2} (R := F) ⊥))))
    (((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) r)⁻¹ : E)

Tactic:
exact ⟨r⁻¹, map_inv₀ _ _⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : IntermediateField F E
⊢ S ⊔ T = adjoin F ((↑S : Set E) ∪ (↑T : Set E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set (IntermediateField F E)
⊢ sSup S = adjoin F (⋃₀ (SetLike.coe '' S))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.sUnion, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ (↑⊥ : Set E) = Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) ⊥ x ↔
    Membership.mem (γ := Set E) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) (toSubalgebra ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_2 + 1} (α := Subfield E) (toSubfield.{u_1, u_2} (K := F) ⊥)
    (RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F E))

Tactic:
rfl

Premises used: Subfield.copy, RingHom.fieldRange, Subsemiring.copy, rfl, RingHom.rangeS
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ (↑⊤ : Set E) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) (toSubalgebra ⊤) ⊤

Tactic:
rfl

Premises used: Subalgebra.copy, rfl