-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
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)
⊢ 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)
have 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))
Tactic: split_ifs with h