-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
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)
⊢ 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)
have 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))
      sorry)
  (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)
Tactic: simp_rw [← ha, ← hb, LinearMap.map_smul_of_tower, LinearMap.smul_apply, smul_smul,
        mul_comm b a, smul_eq_zero_iff_eq]