awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
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)
⊢ 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)
have 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)
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]
-- 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 })
    (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)
have pos : 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) →
  x ≈ x_1
Tactic: split_ifs
-- 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)
pos :
  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) →
    x ≈ x_1
⊢ 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)
have neg : ∀
  (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)),
  HasEquiv.Equiv (α := { v : Fin 3 → F // v ≠ 0 })
    (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)
    (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: split_ifs
-- 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)
h_2 :
  ¬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)
w : Fˣ
⊢ HasEquiv.Equiv (α := { v : Fin 3 → F // v ≠ 0 })
    (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))
      ⋯)
    (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_2)
have h : (fun (m : Fˣ) ↦
      HSMul.hSMul (β := Fin 3 → F) m
        ((↑(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_2) :
            Fin 3 → F) :
          Fin 3 → F))
    (a * b) =
  (↑(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) :
    Fin 3 → F)
Tactic: use a * b
-- 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
⊢ 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 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)
Tactic: split_ifs with h
-- 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
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)
have pos : Eq (α := Quotient (α := { v : Fin 3 → F // v ≠ 0 }) (projectivizationSetoid F (Fin 3 → F)))
  (Quotient.mk''
    (if h : True then Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) v hv
    else Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) 0 sorry))
  (mk F v hv)
Tactic: simp only [h]
-- 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
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))
have neg : Eq (α := Quotient (α := { v : Fin 3 → F // v ≠ 0 }) (projectivizationSetoid F (Fin 3 → F)))
  (Quotient.mk''
      (if h : False then Subtype.mk (p := fun (v : Fin 3 → F) ↦ v ≠ 0) v hv
      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) →ₗ[F] Fin 3 → F) :
              (a : Fin 3 → F) → Fin 3 → F)
            w)
          sorry) :
    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: simp only [h]
-- 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
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 (α := ℙ F (Fin 3 → F)) (cross (mk F v hv) (mk F w hw)) (mk F v hv)
have rw : Eq (α := ℙ F (Fin 3 → F))
  (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)
  (mk F v hv)
Tactic: rw [cross_mk, dif_pos h]