-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ0_Δ : (ofJ0 R).Δ = -27

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ -({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
                2 *
            ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 *
                      { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆ +
                    4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂ *
                      { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆ -
                  { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ *
                      { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ *
                    { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
                { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂ *
                  { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ ^ 2 -
              { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ ^ 2) -
          8 *
            (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
                { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ *
                  { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) ^
              3 -
        27 *
          ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ ^ 2 +
              4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆) ^
            2 +
      9 *
            ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 +
              4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) *
          (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
            { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) *
        ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ ^ 2 +
          4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆) =
    -27

Tactic:
norm_num1

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ (ofJ0 R).Δ = -27

Tactic:
rw [ofJ0, Δ, b₂, b₄, b₆, b₈]

Result:
R : Type u_1
inst✝ : CommRing R
⊢ -({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
                2 *
            ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 *
                      { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆ +
                    4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂ *
                      { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆ -
                  { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ *
                      { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ *
                    { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
                { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂ *
                  { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ ^ 2 -
              { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ ^ 2) -
          8 *
            (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
                { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ *
                  { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) ^
              3 -
        27 *
          ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ ^ 2 +
              4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆) ^
            2 +
      9 *
            ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 +
              4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) *
          (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
            { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) *
        ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃ ^ 2 +
          4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₆) =
    -27