-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 : ℕ)
rw₆ :
  ((↑(adjoinRootEquivAdjoin K hx) : AdjoinRoot (minpoly K x) ≃ₗ[K] ↥K⟮x⟯) : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯)
      ((AdjoinRoot.powerBasis ⋯).gen ^ (↑i : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₇ :
  (adjoinRootEquivAdjoin K hx : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯) ((AdjoinRoot.powerBasis ⋯).gen ^ (↑i : ℕ)) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₈ :
  HPow.hPow (α := ↥K⟮x⟯)
      ((adjoinRootEquivAdjoin K hx : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯) (AdjoinRoot.powerBasis ⋯).gen : ↥K⟮x⟯)
      (↑i : ℕ) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₉ :
  HPow.hPow (α := ↥K⟮x⟯)
      ((adjoinRootEquivAdjoin K hx : (a : AdjoinRoot (minpoly K x)) → ↥K⟮x⟯) (AdjoinRoot.root (minpoly K x)) : ↥K⟮x⟯)
      (↑i : ℕ) =
    HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen K x) (↑i : ℕ)
rw₁₀ rw₁₁ :
  HPow.hPow (α := ↥K⟮x⟯) (AdjoinSimple.gen 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 : ℕ)

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]

Premises used: finCongr_apply, map_pow, PowerBasis.basis_eq_pow, IntermediateField.adjoinRootEquivAdjoin_apply_root, Module.Basis.map_apply, Fin.cast_eq_self, finCongr_symm, IntermediateField.powerBasisAux, Module.Basis.reindex_apply, AdjoinRoot.powerBasis_gen, AlgEquiv.toLinearEquiv_apply