-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_smul (P : Fin 3 → R) {u : R} (hu : IsUnit u) :
    W'.Nonsingular (u • P) ↔ W'.Nonsingular P :=
  have hP {u : R} (hu : IsUnit u) {P : Fin 3 → R} (hP : W'.Nonsingular <| u • P) :
      W'.Nonsingular P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ 2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * (u * P z) ^ 2 = 0

Tactic:
linear_combination (norm := ring1) u ^ 2 * hP'.right.left

Result:
no goals

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) = 0 ∧
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 = 0 ∧
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) =
        0

Tactic:
simp only [smul_fin3_ext]

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u * P y) * (u * P z) - (3 * (u * P x) ^ 2 + 2 * W'.a₂ * (u * P x) * (u * P z) + W'.a₄ * (u * P z) ^ 2) = 0 ∧
    2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * (u * P z) ^ 2 = 0 ∧
      (u * P y) ^ 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
          (W'.a₂ * (u * P x) ^ 2 + 2 * W'.a₄ * (u * P x) * (u * P z) + 3 * W'.a₆ * (u * P z) ^ 2) =
        0

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u * P y) * (u * P z) - (3 * (u * P x) ^ 2 + 2 * W'.a₂ * (u * P x) * (u * P z) + W'.a₄ * (u * P z) ^ 2) = 0 ∧
    2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * (u * P z) ^ 2 = 0 ∧
      (u * P y) ^ 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
          (W'.a₂ * (u * P x) ^ 2 + 2 * W'.a₄ * (u * P x) * (u * P z) + 3 * W'.a₆ * (u * P z) ^ 2) =
        0

Tactic:
exact ⟨by linear_combination (norm := ring1) u ^ 2 * hP'.left,
  by linear_combination (norm := ring1) u ^ 2 * hP'.right.left,
  by linear_combination (norm := ring1) u ^ 2 * hP'.right.right⟩

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ (u * P y) ^ 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
      (W'.a₂ * (u * P x) ^ 2 + 2 * W'.a₄ * (u * P x) * (u * P z) + 3 * W'.a₆ * (u * P z) ^ 2) =
    0

Tactic:
linear_combination (norm := ring1) u ^ 2 * hP'.right.right

Result:
no goals

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) ≠ 0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 ≠ 0 ∨
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) ≠
        0
⊢ W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) ≠ 0 ∨
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 ≠ 0 ∨
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) ≠
        0

Tactic:
contrapose! hP'

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) = 0 ∧
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 = 0 ∧
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) =
        0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular (↑hu.unit⁻¹ • u • P)

Tactic:
rwa [smul_smul, hu.val_inv_mul, one_smul]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP : W'.Nonsingular (u • P)
⊢ W'.Nonsingular P

Tactic:
rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) ≠ 0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 ≠ 0 ∨
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) ≠
        0
⊢ W'.Nonsingular P