-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
h : Nontrivial R
rw :
  (⋯.by_cases (fun (x : Subsingleton R) ↦ default) fun (x : Nontrivial R) ↦
          Basis.reindex (ι :=
            Fin
              (PowerBasis.dim.{r, r} (R := R[X]) (S := AdjoinRoot (R := R[X]) W'.polynomial)
                (AdjoinRoot.powerBasis' ⋯)))
            (PowerBasis.basis (AdjoinRoot.powerBasis' ⋯)) (finCongr ⋯) :
        (a : Fin 2) → W'.CoordinateRing)
      n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
rw₁ :
  (if hp : Subsingleton R then default
        else
          Basis.reindex (ι :=
            Fin
              (PowerBasis.dim.{r, r} (R := R[X]) (S := AdjoinRoot (R := R[X]) W'.polynomial)
                (AdjoinRoot.powerBasis' ⋯)))
            (PowerBasis.basis (AdjoinRoot.powerBasis' ⋯)) (finCongr ⋯) :
        (a : Fin 2) → W'.CoordinateRing)
      n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
rw₂ :
  (Basis.reindex (ι :=
          Fin
            (PowerBasis.dim.{r, r} (R := R[X]) (S := AdjoinRoot (R := R[X]) W'.polynomial) (AdjoinRoot.powerBasis' ⋯)))
          (PowerBasis.basis (AdjoinRoot.powerBasis' ⋯)) (finCongr ⋯) :
        (a : Fin 2) → W'.CoordinateRing)
      n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
rw₃ :
  (PowerBasis.basis (AdjoinRoot.powerBasis' ⋯) : (a : Fin (AdjoinRoot.powerBasis' ⋯).dim) → AdjoinRoot W'.polynomial)
      ((Equiv.symm (finCongr ⋯) : (a : Fin 2) → Fin (AdjoinRoot.powerBasis' ⋯).dim) n :
        Fin
          (PowerBasis.dim.{r, r} (R := R[X]) (S := AdjoinRoot (R := R[X]) W'.polynomial) (AdjoinRoot.powerBasis' ⋯))) =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
rw₄ :
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯))
      (↑((Equiv.symm (finCongr ⋯) : (a : Fin 2) → Fin (AdjoinRoot.powerBasis' ⋯).dim) n) : ℕ) =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
rw₅ :
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯))
      (↑(Fin.cast ⋯ n) : ℕ) =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
rw₆ rw₇ :
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ) =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)

Tactic:
rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
    PowerBasis.basis_eq_pow, finCongr_symm_apply, Fin.val_cast]

Premises used: dif_neg, PowerBasis.basis_eq_pow, WeierstrassCurve.Affine.CoordinateRing.basis, Or.by_cases, finCongr_symm_apply, not_subsingleton, Fin.val_cast, Module.Basis.reindex_apply