-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ (r₁ : R), (algebraMap R K : (a : R) → K) r₁ = W.a₁
h₂ : ∃ (r₂ : R), (algebraMap R K : (a : R) → K) r₂ = W.a₂
h₃ : ∃ (r₃ : R), (algebraMap R K : (a : R) → K) r₃ = W.a₃
h₄ : ∃ (r₄ : R), (algebraMap R K : (a : R) → K) r₄ = W.a₄
h₆ : ∃ (r₆ : R), (algebraMap R K : (a : R) → K) r₆ = W.a₆
h :
  W.a₁ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₁
h₅ :
  W.a₂ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₂
h₇ :
  W.a₃ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₃
h₈ :
  W.a₄ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₄
⊢ W =
    { a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
        a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
        a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
        a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
        a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K
have h₉ : W.a₆ =
  ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
        a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
        a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
        a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
        a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₆
Tactic: ext