-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
pos :
  ∀
    (h :
      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 (α := Quotient (α := { v : Fin 3 → F // v ≠ 0 }) (projectivizationSetoid F (Fin 3 → F)))
      (Quotient.mk''
        ((fun (v w : { v : Fin 3 → F // v ≠ 0 }) ↦
            (if h :
                  Eq (α := Fin 3 → F)
                    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑v : Fin 3 → F) :
                            (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                          (a : Fin 3 → F) → Fin 3 → F)
                        (↑w : Fin 3 → F) :
                      Fin 3 → F)
                    (0 : Fin 3 → F) then
                v
              else
                Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0)
                  ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑v : Fin 3 → F) :
                        (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                      (a : Fin 3 → F) → Fin 3 → F)
                    (↑w : Fin 3 → F))
                  h :
              { v : Fin 3 → F // v ≠ 0 }))
          (Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) v hv) (Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) w hw)))
      (mk F v hv)
neg :
  ∀
    (h :
      ¬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 (α := Quotient (α := { v : Fin 3 → F // v ≠ 0 }) (projectivizationSetoid F (Fin 3 → F)))
      (Quotient.mk''
          ((fun (v w : { v : Fin 3 → F // v ≠ 0 }) ↦
              (if h :
                    Eq (α := Fin 3 → F)
                      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑v : Fin 3 → F) :
                              (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                            (a : Fin 3 → F) → Fin 3 → F)
                          (↑w : Fin 3 → F) :
                        Fin 3 → F)
                      (0 : Fin 3 → F) then
                  v
                else
                  Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0)
                    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑v : Fin 3 → F) :
                          (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                        (a : Fin 3 → F) → Fin 3 → F)
                      (↑w : Fin 3 → F))
                    h :
                { v : Fin 3 → F // v ≠ 0 }))
            (Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) v hv) (Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) w hw)) :
        Quotient (α := { v : Fin 3 → F // v ≠ 0 }) (projectivizationSetoid F (Fin 3 → F)))
      (mk 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)
          h :
        ℙ F (Fin 3 → F))
⊢ Eq.{u_1 + 1} (α := Quotient (α := { v : Fin 3 → F // v ≠ 0 }) (projectivizationSetoid F (Fin 3 → F)))
    (Quotient.mk''
      ((fun (v w : { v : Fin 3 → F // v ≠ 0 }) ↦
          (if h :
                Eq (α := Fin 3 → F)
                  ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑v : Fin 3 → F) :
                          (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                        (a : Fin 3 → F) → Fin 3 → F)
                      (↑w : Fin 3 → F) :
                    Fin 3 → F)
                  (0 : Fin 3 → F) then
              v
            else
              Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0)
                ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑v : Fin 3 → F) :
                      (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                    (a : Fin 3 → F) → Fin 3 → F)
                  (↑w : Fin 3 → F))
                h :
            { v : Fin 3 → F // v ≠ 0 }))
        (Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) v hv) (Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) w hw)))
    (if h :
        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) then
      mk F v hv
    else
      mk 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)
        h)

Tactic:
split_ifs with h