awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Affine R
inst_4 : Algebra R S
inst_5 : DecidableEq F
inst_6 : DecidableEq K
inst_7 : Algebra R F
inst_8 : Algebra S F
inst_9 : IsScalarTower R S F
inst_10 : Algebra R K
inst_11 : Algebra S K
inst_12 : IsScalarTower R S K
f : F →ₐ[S] K
x₁ x₂ y₁ y₂ : F
rw :
  (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂) =
    ((↑f : F →+* K) : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)
rw₁ :
  (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂) =
    ((W'⁄F).map (↑f : F →+* K)).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂)
⊢ (W'⁄K).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)
have rw₂ : (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂) (((↑f : F →+* K) : (a : F) → K) y₁)
    (((↑f : F →+* K) : (a : F) → K) y₂) =
  (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
    (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂)
Tactic: rw [← RingHom.coe_coe, ← map_slope, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
h : Nontrivial R
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have rw : (sorry.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' sorry)))
          (PowerBasis.basis (AdjoinRoot.powerBasis' sorry)) (finCongr sorry) :
      (a : Fin 2) → W'.CoordinateRing)
    n =
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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 : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have 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' sorry)))
          (PowerBasis.basis (AdjoinRoot.powerBasis' sorry)) (finCongr sorry) :
      (a : Fin 2) → W'.CoordinateRing)
    n =
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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 : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have rw₂ : (Basis.reindex (ι :=
        Fin (PowerBasis.dim.{r, r} (R := R[X]) (S := AdjoinRoot (R := R[X]) W'.polynomial) (AdjoinRoot.powerBasis' sorry)))
        (PowerBasis.basis (AdjoinRoot.powerBasis' sorry)) (finCongr sorry) :
      (a : Fin 2) → W'.CoordinateRing)
    n =
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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 : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have rw₃ : (PowerBasis.basis (AdjoinRoot.powerBasis' sorry) : (a : Fin (AdjoinRoot.powerBasis' sorry).dim) → AdjoinRoot W'.polynomial)
    ((Equiv.symm (finCongr sorry) : (a : Fin 2) → Fin (AdjoinRoot.powerBasis' sorry).dim) n :
      Fin (PowerBasis.dim.{r, r} (R := R[X]) (S := AdjoinRoot (R := R[X]) W'.polynomial) (AdjoinRoot.powerBasis' sorry))) =
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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 : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have rw₄ : HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry))
    (↑((Equiv.symm (finCongr sorry) : (a : Fin 2) → Fin (AdjoinRoot.powerBasis' sorry).dim) n) : ℕ) =
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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 : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have rw₅ : HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry))
    (↑(Fin.cast sorry n) : ℕ) =
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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 : ℕ)
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have rw₆ : HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑n : ℕ) =
  HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
⊢ (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' ⋯)) (↑n : ℕ)
have nontriviality : Subsingleton R →
  (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑n : ℕ)
Tactic: classical
  nontriviality R
  rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
    PowerBasis.basis_eq_pow, finCongr_symm_apply, Fin.val_cast]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
nontriviality :
  Subsingleton R →
    (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) 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 : ℕ)
have nontriviality₁ : Nontrivial R →
  (CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n =
    HPow.hPow (α := AdjoinRoot (R := R[X]) W'.polynomial) (PowerBasis.gen (AdjoinRoot.powerBasis' sorry)) (↑n : ℕ)
Tactic: classical
  nontriviality R
  rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
    PowerBasis.basis_eq_pow, finCongr_symm_apply, Fin.val_cast]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Eq (α := (a : Fin 2) → W'.CoordinateRing) (⇑(CoordinateRing.basis W') : (a : Fin 2) → W'.CoordinateRing)
    ![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y]
have h : ∀ (n : Fin 2),
  Eq (α := W'.CoordinateRing) ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] n : W'.CoordinateRing)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
⊢ Eq (α := W'.CoordinateRing) ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] n : W'.CoordinateRing)
have h : Eq (α := W'.CoordinateRing)
  ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : W'.CoordinateRing)
  (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : W'.CoordinateRing)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
n : Fin 2
h :
  Eq (α := W'.CoordinateRing)
    ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : W'.CoordinateRing)
⊢ Eq (α := W'.CoordinateRing) ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) n : W'.CoordinateRing)
    (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] n : W'.CoordinateRing)
have h₁ : Eq (α := W'.CoordinateRing)
  ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : W'.CoordinateRing)
  (![1, (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : W'.CoordinateRing)
Tactic: fin_cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
hpq :
  HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
⊢ p = 0 ∧ q = 0
have h : Eq.{r + 1} (α := W'.CoordinateRing)
    (∑ i : Fin 2,
      HSMul.hSMul (β := W'.CoordinateRing) (![p, q] i)
        ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing))
    0 →
  ∀ (i : Fin 2), ![p, q] i = 0
Tactic: have h := Fintype.linearIndependent_iff.mp (CoordinateRing.basis W').linearIndependent ![p, q]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
hpq :
  HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
h :
  Eq.{r + 1} (α := W'.CoordinateRing)
      (∑ i : Fin 2,
        HSMul.hSMul (β := W'.CoordinateRing) (![p, q] i)
          ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing))
      0 →
    ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0
have h₁ : HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 0) 1 +
      HSMul.hSMul (β := W'.CoordinateRing) (![p, q] 1) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0 →
  ∀ (i : Fin 2), ![p, q] i = 0
Tactic: rw [Fin.sum_univ_succ, basis_zero, Fin.sum_univ_one, Fin.succ_zero_eq_one, basis_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x : W'.CoordinateRing
⊢ ∃ (p : R[X]) (q : R[X]),
    HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      x
have h : ∑ i : Fin 2,
    HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
      ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x i : R[X])
      ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing) =
  x
Tactic: have h := (CoordinateRing.basis W').sum_equivFun x