awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have rw : Eq (α := ↥K⟮y⟯)
  (((adjoinRootEquivAdjoin K sorry).symm.trans
          (AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K sorry)) :
        (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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have rw₁ : Eq.{u_2 + 1} (α := ↥K⟮y⟯)
  ((AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K sorry) :
        (a : AdjoinRoot (minpoly K x)) → ↥K⟮y⟯)
      (((adjoinRootEquivAdjoin K sorry).symm : (a : ↥K⟮x⟯) → AdjoinRoot (minpoly K x)) (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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have rw₂ : Eq.{u_2 + 1} (α := ↥K⟮y⟯)
  ((AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K sorry) :
        (a : AdjoinRoot (minpoly K x)) → ↥K⟮y⟯)
      (((adjoinRootEquivAdjoin K sorry).symm : (a : ↥K⟮x⟯) → AdjoinRoot (minpoly K x))
        ((adjoinRootEquivAdjoin K sorry : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯) (AdjoinRoot.root (minpoly 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have rw₃ : Eq.{u_2 + 1} (α := ↥K⟮y⟯)
  ((AlgEquiv.trans (AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (adjoinRootEquivAdjoin K sorry) :
        (a : AdjoinRoot (minpoly K x)) → ↥K⟮y⟯)
      (AdjoinRoot.root (minpoly 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have rw₄ : Eq.{u_2 + 1} (α := ↥K⟮y⟯)
  ((adjoinRootEquivAdjoin K sorry : (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⟯)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have rw₅ : Eq.{u_2 + 1} (α := ↥K⟮y⟯)
  ((adjoinRootEquivAdjoin K sorry : (a : AdjoinRoot (minpoly K y)) → ↥K⟮y⟯) (AdjoinRoot.root (minpoly K y)) : ↥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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have rw₆ : Eq (α := ↥K⟮y⟯) (AdjoinSimple.gen K y) (AdjoinSimple.gen 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ Eq (α := K[X]) (minpoly K (adjoin.powerBasis ⋯).gen) (minpoly K pb.gen)
have rw : Eq (α := K[X]) (minpoly K (B := ↥K⟮pb.gen⟯) (AdjoinSimple.gen K pb.gen)) (minpoly K pb.gen)
Tactic: rw [adjoin.powerBasis_gen, minpoly_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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)
⊢ Eq (α := K[X]) (minpoly K (adjoin.powerBasis ⋯).gen) (minpoly K pb.gen)
have rw₁ : Eq (α := K[X]) (minpoly K pb.gen) (minpoly K pb.gen)
Tactic: rw [adjoin.powerBasis_gen, minpoly_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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 (α := ↥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⟯)
have rw : Eq (α := ↥K⟮pb.gen⟯)
  ((((adjoin.powerBasis sorry).equivOfMinpoly pb sorry).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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ 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⟯)
have rw₁ : Eq (α := ↥K⟮pb.gen⟯)
  ((pb.equivOfMinpoly (adjoin.powerBasis sorry) sorry : (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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ 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⟯)
have rw₂ : Eq.{u_2 + 1} (α := ↥K⟮pb.gen⟯) ((aeval (adjoin.powerBasis sorry).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⟯)
Tactic: rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_aeval, adjoin.powerBasis_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ 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⟯)
have 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⟯)
Tactic: rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_aeval, adjoin.powerBasis_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ 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⟯)
have rw : Eq (α := ↥K⟮pb.gen⟯) ((((adjoin.powerBasis sorry).equivOfMinpoly pb sorry).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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ 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⟯)
have rw₁ : Eq (α := ↥K⟮pb.gen⟯) ((pb.equivOfMinpoly (adjoin.powerBasis sorry) sorry : (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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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⟯)
⊢ 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⟯)
have rw₂ : (adjoin.powerBasis sorry).gen = AdjoinSimple.gen K pb.gen
Tactic: rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ 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⟯)
have rw₃ : Eq (α := ↥K⟮pb.gen⟯) (AdjoinSimple.gen K pb.gen) (AdjoinSimple.gen K pb.gen)
Tactic: rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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} #↥(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))) ℵ₀
have 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))) ℵ₀
Tactic: apply (Cardinal.lift_le.mpr (Subfield.cardinalMk_closure_le_max _)).trans
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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} (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))) ℵ₀
have 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))) ℵ₀
Tactic: rw [lift_max, sup_le_iff, lift_aleph0]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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))) ℵ₀
have 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))) ℵ₀
Tactic: refine ⟨(Cardinal.lift_le.mpr ((mk_union_le _ _).trans <| add_le_max _ _)).trans ?_, le_sup_right⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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}
      (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))) ℵ₀
have 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))) ℵ₀
Tactic: simp_rw [lift_max, lift_aleph0]