-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma nonsingular_iff_variableChange (x y : R) :
    W'.Nonsingular x y ↔ (W'.variableChange ⟨1, x, 0, y⟩).toAffine.Nonsingular 0 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ ↑1⁻¹ ^ 6 * (W'.a₆ + x * W'.a₄ + x ^ 2 * W'.a₂ + x ^ 3 - y * W'.a₃ - y ^ 2 - x * y * W'.a₁) = 0 ∧
      (2 * y + W'.a₁ * x + W'.a₃ ≠ 0 ∨ -(W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)) ≠ 0) ↔
    ↑1⁻¹ ^ 6 * (W'.a₆ + x * W'.a₄ + x ^ 2 * W'.a₂ + x ^ 3 - y * W'.a₃ - y ^ 2 - x * y * W'.a₁) = 0 ∧
      (1 ^ 3 * (W'.a₃ + x * W'.a₁ + 2 * y) ≠ 0 ∨
        1 ^ 4 * (W'.a₄ - 0 * W'.a₃ + 2 * x * W'.a₂ - (y + x * 0) * W'.a₁ + 3 * x ^ 2 - 2 * 0 * y) ≠ 0)

Tactic:
congr! 3 <;> ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Nonsingular x y ↔ (variableChange W' { u := 1, r := x, s := 0, t := y }).toAffine.Nonsingular 0 0

Tactic:
rw [nonsingular_iff', equation_iff_variableChange, equation_zero, ← neg_ne_zero, or_comm,
  nonsingular_zero, variableChange_a₃, variableChange_a₄, inv_one, Units.val_one]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ (variableChange W' { u := 1, r := x, s := 0, t := y }).toAffine.a₆ = 0 ∧
      (2 * y + W'.a₁ * x + W'.a₃ ≠ 0 ∨ -(W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)) ≠ 0) ↔
    (variableChange W' { u := 1, r := x, s := 0, t := y }).toAffine.a₆ = 0 ∧
      (1 ^ 3 * (W'.a₃ + { u := 1, r := x, s := 0, t := y }.r * W'.a₁ + 2 * { u := 1, r := x, s := 0, t := y }.t) ≠ 0 ∨
        1 ^ 4 *
            (W'.a₄ - { u := 1, r := x, s := 0, t := y }.s * W'.a₃ + 2 * { u := 1, r := x, s := 0, t := y }.r * W'.a₂ -
                  ({ u := 1, r := x, s := 0, t := y }.t +
                      { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.s) *
                    W'.a₁ +
                3 * { u := 1, r := x, s := 0, t := y }.r ^ 2 -
              2 * { u := 1, r := x, s := 0, t := y }.s * { u := 1, r := x, s := 0, t := y }.t) ≠
          0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ (variableChange W' { u := 1, r := x, s := 0, t := y }).toAffine.a₆ = 0 ∧
      (2 * y + W'.a₁ * x + W'.a₃ ≠ 0 ∨ -(W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)) ≠ 0) ↔
    (variableChange W' { u := 1, r := x, s := 0, t := y }).toAffine.a₆ = 0 ∧
      (1 ^ 3 * (W'.a₃ + { u := 1, r := x, s := 0, t := y }.r * W'.a₁ + 2 * { u := 1, r := x, s := 0, t := y }.t) ≠ 0 ∨
        1 ^ 4 *
            (W'.a₄ - { u := 1, r := x, s := 0, t := y }.s * W'.a₃ + 2 * { u := 1, r := x, s := 0, t := y }.r * W'.a₂ -
                  ({ u := 1, r := x, s := 0, t := y }.t +
                      { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.s) *
                    W'.a₁ +
                3 * { u := 1, r := x, s := 0, t := y }.r ^ 2 -
              2 * { u := 1, r := x, s := 0, t := y }.s * { u := 1, r := x, s := 0, t := y }.t) ≠
          0)

Tactic:
simp only [variableChange]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ ↑1⁻¹ ^ 6 * (W'.a₆ + x * W'.a₄ + x ^ 2 * W'.a₂ + x ^ 3 - y * W'.a₃ - y ^ 2 - x * y * W'.a₁) = 0 ∧
      (2 * y + W'.a₁ * x + W'.a₃ ≠ 0 ∨ -(W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)) ≠ 0) ↔
    ↑1⁻¹ ^ 6 * (W'.a₆ + x * W'.a₄ + x ^ 2 * W'.a₂ + x ^ 3 - y * W'.a₃ - y ^ 2 - x * y * W'.a₁) = 0 ∧
      (1 ^ 3 * (W'.a₃ + x * W'.a₁ + 2 * y) ≠ 0 ∨
        1 ^ 4 * (W'.a₄ - 0 * W'.a₃ + 2 * x * W'.a₂ - (y + x * 0) * W'.a₁ + 3 * x ^ 2 - 2 * 0 * y) ≠ 0)