awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
hx : Membership.mem (γ := Set E) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
⊢ x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
have right : ∀ (y : F) (hy : (algebraMap F E : (a : F) → E) y = x),
  x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
Tactic: obtain ⟨y, hy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
⊢ x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
have right : (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
    ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y : AdjoinRoot (minpoly F α)) =
  x
Tactic: refine ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
⊢ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
      ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y : AdjoinRoot (minpoly F α)) =
    x
have right : (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯.toSubfield) → E)
    ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯.toSubfield)
        ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y) :
      ↥(toSubfield F⟮α⟯)) =
  x
Tactic: rw [RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
          ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y) :
        ↥F⟮α⟯) =
    x
have right : (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
    ((((↑(Algebra.ofId F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : (a : F) → ↥F⟮α⟯) y :
      ↥F⟮α⟯) =
  x
Tactic: rw [AdjoinRoot.lift_of (aeval_gen_minpoly F α)]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ {α} ⊆ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
have right : (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
    (AdjoinRoot.root (minpoly F α)) =
  α
Tactic: refine Set.singleton_subset_iff.mpr ⟨AdjoinRoot.root (minpoly F α), ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
      (AdjoinRoot.root (minpoly F α)) =
    α
have right : (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯.toSubfield) → E)
    ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯.toSubfield) (AdjoinRoot.root (minpoly F α)) : ↥(toSubfield F⟮α⟯)) =
  α
Tactic: rw [RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯) (AdjoinRoot.root (minpoly F α)) : ↥F⟮α⟯) =
    α
have right : (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α) = α
Tactic: rw [AdjoinRoot.lift_root (aeval_gen_minpoly F α)]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
h : IsIntegral F α
⊢ Eq.{u_1 + 1} (α := AdjoinRoot (minpoly F α))
    (((adjoinRootEquivAdjoin F h).symm : (a : ↥F⟮α⟯) → AdjoinRoot (minpoly F α)) (AdjoinSimple.gen F α) :
      AdjoinRoot (minpoly F α))
    (AdjoinRoot.root (minpoly F α) : AdjoinRoot (minpoly F α))
have rw : Eq (α := ↥F⟮α⟯) (AdjoinSimple.gen F α)
  ((adjoinRootEquivAdjoin F h : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯) (AdjoinRoot.root (minpoly F α)))
Tactic: rw [AlgEquiv.symm_apply_eq, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
h : IsIntegral F α
rw :
  Eq (α := ↥F⟮α⟯) (AdjoinSimple.gen F α)
    ((adjoinRootEquivAdjoin F h : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯) (AdjoinRoot.root (minpoly F α)))
⊢ Eq.{u_1 + 1} (α := AdjoinRoot (minpoly F α))
    (((adjoinRootEquivAdjoin F h).symm : (a : ↥F⟮α⟯) → AdjoinRoot (minpoly F α)) (AdjoinSimple.gen F α) :
      AdjoinRoot (minpoly F α))
    (AdjoinRoot.root (minpoly F α) : AdjoinRoot (minpoly F α))
have rw₁ : Eq (α := ↥F⟮α⟯) (AdjoinSimple.gen F α) (AdjoinSimple.gen F α)
Tactic: rw [AlgEquiv.symm_apply_eq, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯) i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
have rw : (((AdjoinRoot.powerBasis sorry).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯)).reindex
        (finCongr sorry) :
      (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯)
    i =
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
Tactic: rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
rw :
  (((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯)).reindex
          (finCongr ⋯) :
        (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯)
      i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯) i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
have rw₁ : ((AdjoinRoot.powerBasis sorry).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) :
      (a : Fin (AdjoinRoot.powerBasis sorry).dim) → ↥K⟮x⟯)
    (((finCongr sorry).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis sorry).dim) i :
      Fin (AdjoinRoot.powerBasis sorry).dim) =
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
Tactic: rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
rw :
  (((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯)).reindex
          (finCongr ⋯) :
        (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯)
      i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₁ :
  ((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) :
        (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → ↥K⟮x⟯)
      (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
        Fin (AdjoinRoot.powerBasis ⋯).dim) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯) i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
have rw₂ : ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
    (((AdjoinRoot.powerBasis sorry).basis : (a : Fin (AdjoinRoot.powerBasis sorry).dim) → AdjoinRoot (minpoly K x))
      (((finCongr sorry).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis sorry).dim) i :
        Fin (AdjoinRoot.powerBasis sorry).dim)) =
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
Tactic: rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
rw :
  (((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯)).reindex
          (finCongr ⋯) :
        (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯)
      i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₁ :
  ((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) :
        (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → ↥K⟮x⟯)
      (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
        Fin (AdjoinRoot.powerBasis ⋯).dim) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₂ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      (((AdjoinRoot.powerBasis ⋯).basis : (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → AdjoinRoot (minpoly K x))
        (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
          Fin (AdjoinRoot.powerBasis ⋯).dim)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯) i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
have rw₃ : ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
    ((AdjoinRoot.powerBasis sorry).gen ^
      (↑(((finCongr sorry).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis sorry).dim) i) : ℕ)) =
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
Tactic: rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
rw :
  (((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯)).reindex
          (finCongr ⋯) :
        (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯)
      i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₁ :
  ((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) :
        (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → ↥K⟮x⟯)
      (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
        Fin (AdjoinRoot.powerBasis ⋯).dim) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₂ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      (((AdjoinRoot.powerBasis ⋯).basis : (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → AdjoinRoot (minpoly K x))
        (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
          Fin (AdjoinRoot.powerBasis ⋯).dim)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₃ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      ((AdjoinRoot.powerBasis ⋯).gen ^
        (↑(((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i) : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯) i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
have rw₄ : ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
    ((AdjoinRoot.powerBasis sorry).gen ^
      (↑((finCongr sorry : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis sorry).dim) i) : ℕ)) =
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
Tactic: rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
rw :
  (((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯)).reindex
          (finCongr ⋯) :
        (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯)
      i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₁ :
  ((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) :
        (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → ↥K⟮x⟯)
      (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
        Fin (AdjoinRoot.powerBasis ⋯).dim) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₂ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      (((AdjoinRoot.powerBasis ⋯).basis : (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → AdjoinRoot (minpoly K x))
        (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
          Fin (AdjoinRoot.powerBasis ⋯).dim)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₃ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      ((AdjoinRoot.powerBasis ⋯).gen ^
        (↑(((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i) : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₄ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      ((AdjoinRoot.powerBasis ⋯).gen ^
        (↑((finCongr ⋯ : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i) : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯) i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
have rw₅ : ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
    ((AdjoinRoot.powerBasis sorry).gen ^ (↑(Fin.cast sorry i) : ℕ)) =
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
Tactic: rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
rw :
  (((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯)).reindex
          (finCongr ⋯) :
        (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯)
      i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₁ :
  ((AdjoinRoot.powerBasis ⋯).basis.map (↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) :
        (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → ↥K⟮x⟯)
      (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
        Fin (AdjoinRoot.powerBasis ⋯).dim) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₂ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      (((AdjoinRoot.powerBasis ⋯).basis : (a : Fin (AdjoinRoot.powerBasis ⋯).dim) → AdjoinRoot (minpoly K x))
        (((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i :
          Fin (AdjoinRoot.powerBasis ⋯).dim)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₃ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      ((AdjoinRoot.powerBasis ⋯).gen ^
        (↑(((finCongr ⋯).symm : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i) : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₄ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      ((AdjoinRoot.powerBasis ⋯).gen ^
        (↑((finCongr ⋯ : (a : Fin (minpoly K x).natDegree) → Fin (AdjoinRoot.powerBasis ⋯).dim) i) : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₅ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      ((AdjoinRoot.powerBasis ⋯).gen ^ (↑(Fin.cast ⋯ i) : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K⟮x⟯) i =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
have rw₆ : ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
    ((AdjoinRoot.powerBasis sorry).gen ^ (↑i : ℕ)) =
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
Tactic: rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]