-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
inst_2 : DecidableEq F
x x_1 : { v : Fin 3 → F // v ≠ 0 }
h : x ≈ x_1
x_2 x_3 : { v : Fin 3 → F // v ≠ 0 }
h_1 : x_2 ≈ x_3
a : Fˣ
ha : (fun (m : Fˣ) ↦ m • (↑x_1 : Fin 3 → F)) a = (↑x : Fin 3 → F)
b : Fˣ
hb : (fun (m : Fˣ) ↦ m • (↑x_3 : Fin 3 → F)) b = (↑x_2 : Fin 3 → F)
simp_rw :
  HasEquiv.Equiv.{u_1 + 1, 0} (α := { v : Fin 3 → F // v ≠ 0 })
    (if h :
        Eq (α := Fin 3 → F)
          ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑x_1 : Fin 3 → F) :
                  (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                (a : Fin 3 → F) → Fin 3 → F)
              (↑x_3 : Fin 3 → F) :
            Fin 3 → F)
          (0 : Fin 3 → F) then
      x
    else
      Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0)
        (HSMul.hSMul (β := Fin 3 → F) (a * b)
          ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑x_1 : Fin 3 → F) :
                  (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                (a : Fin 3 → F) → Fin 3 → F)
              (↑x_3 : Fin 3 → F) :
            Fin 3 → F))
        ⋯)
    (if h :
        Eq (α := Fin 3 → F)
          ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑x_1 : Fin 3 → F) :
                  (Fin 3 → F) →ₗ[F] Fin 3 → F) :
                (a : Fin 3 → F) → Fin 3 → F)
              (↑x_3 : Fin 3 → F) :
            Fin 3 → F)
          (0 : Fin 3 → F) then
      x_1
    else
      Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0)
        ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) (↑x_1 : Fin 3 → F) :
              (Fin 3 → F) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → Fin 3 → F)
          (↑x_3 : Fin 3 → F))
        h)
⊢ HasEquiv.Equiv.{u_1 + 1, 0} (α := { v : Fin 3 → F // v ≠ 0 })
    ((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 }))
      x x_2)
    ((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 }))
      x_1 x_3)

Tactic:
simp_rw [← ha, ← hb, LinearMap.map_smul_of_tower, LinearMap.smul_apply, smul_smul,
        mul_comm b a, smul_eq_zero_iff_eq]

Premises used: smul_eq_zero_iff_eq, LinearMap.smul_apply, smul_smul, mul_comm, LinearMap.map_smul_of_tower