-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
rw :
  ¬Eq (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw) ↔
    ¬Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
rw₁ :
  (¬∃ (a : F), a • w = v) ↔
    ¬Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
rw₂ :
  (∀ (x : F), ¬x • w = v) ↔
    ¬Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
rw₃ :
  LinearIndependent F ![w, v] ↔
    ¬Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
rw₄ :
  Ne (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) w : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          v :
        Fin 3 → F)
      (0 : Fin 3 → F) ↔
    ¬Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
rw₅ :
  Ne (α := Fin 3 → F)
      (-(((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
        Fin 3 → F)
      (0 : Fin 3 → F) ↔
    ¬Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
rw₆ rw₇ :
  Ne (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F) ↔
    ¬Eq (α := Fin 3 → F)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w :
          Fin 3 → F)
        (0 : Fin 3 → F)
⊢ Eq (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw) ↔
    Eq (α := Fin 3 → F)
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          w :
        Fin 3 → F)
      (0 : Fin 3 → F)

Tactic:
rw [← not_iff_not, mk_eq_mk_iff', not_exists, ← LinearIndependent.pair_iff' hw,
    ← crossProduct_ne_zero_iff_linearIndependent, ← cross_anticomm, neg_ne_zero]

Premises used: not_iff_not, cross_anticomm, not_exists, LinearIndependent.pair_iff', crossProduct_ne_zero_iff_linearIndependent, neg_ne_zero, Projectivization.mk_eq_mk_iff'