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
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)
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)
⊢ 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)) (mk F v hv) (mk F v hv)
Tactic: rw [cross_mk, dif_pos 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 :
  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 (α := ℙ F (Fin 3 → F)) (cross (mk F v hv) (mk F w hw))
    (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 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 :
    ℙ 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: rw [cross_mk, dif_neg 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 :
  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)
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 :
      ℙ 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 (α := ℙ F (Fin 3 → F)) (cross (mk F v hv) (mk F w hw))
    (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 rw₁ : Eq (α := ℙ 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))
  (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: rw [cross_mk, dif_neg h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
⊢ cross (mk F v hv) (mk F v hv) = mk F v hv
have 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)
      v :
    Fin 3 → F)
  (0 : Fin 3 → F)
Tactic: rw [cross_mk_of_cross_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
⊢ 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)
        v :
      Fin 3 → F)
    (0 : Fin 3 → F)
have h : Eq (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F v hv)
Tactic: rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v
have h : ∀ (v : Fin 3 → F) (hv : v ≠ 0), cross (mk F v hv) (mk F v hv) = mk F v hv
Tactic: induction v with | h v hv =>
  rw [cross_mk_of_cross_eq_zero]
  rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]
Cleared hypotheses: v
-- 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 : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
⊢ Eq (α := ℙ F (Fin 3 → F)) (cross (mk F v hv) (mk F w hw))
    (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)
      ⋯)
have rw : Eq (α := ℙ 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)
      sorry :
    ℙ 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)
      sorry :
    ℙ F (Fin 3 → F))
Tactic: rw [cross_mk_of_cross_ne_zero]
-- 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 : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
rw :
  Eq (α := ℙ 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)
        ⋯ :
      ℙ 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)
        ⋯ :
      ℙ F (Fin 3 → F))
⊢ Eq (α := ℙ F (Fin 3 → F)) (cross (mk F v hv) (mk F w hw))
    (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)
      ⋯)
have h₁ : 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)
Tactic: rw [cross_mk_of_cross_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
⊢ v.cross w = w.cross v
have inl : v.cross v = v.cross v
Tactic: rcases eq_or_ne v w with rfl | h
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
inl : v.cross v = v.cross v
⊢ v.cross w = w.cross v
have inr : ∀ (h : v ≠ w), v.cross w = w.cross v
Tactic: rcases eq_or_ne v w with rfl | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
⊢ cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
have inr : 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)
    sorry =
  cross (mk F w hw) (mk F v hv)
Tactic: rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
inr :
  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)
      ⋯ =
    cross (mk F w hw) (mk F v hv)
⊢ cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
have inr₁ : Eq (α := ℙ 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)
      sorry :
    ℙ F (Fin 3 → F))
  (mk 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)
      sorry :
    ℙ F (Fin 3 → F))
Tactic: rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
inr :
  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)
      ⋯ =
    cross (mk F w hw) (mk F v hv)
inr₁ :
  Eq (α := ℙ 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)
        ⋯ :
      ℙ F (Fin 3 → F))
    (mk 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)
        ⋯ :
      ℙ F (Fin 3 → F))
⊢ cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
have inr₂ : Eq (α := Fin 3 → F)
  ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
        (a : Fin 3 → F) → 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) :
    Fin 3 → F)
  (0 : Fin 3 → F)
Tactic: rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
inr :
  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)
      ⋯ =
    cross (mk F w hw) (mk F v hv)
inr₁ :
  Eq (α := ℙ 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)
        ⋯ :
      ℙ F (Fin 3 → F))
    (mk 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)
        ⋯ :
      ℙ F (Fin 3 → F))
inr₂ :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
⊢ cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
have inr₃ : Eq (α := Fin 3 → F)
  ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
        (a : Fin 3 → F) → 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) :
    Fin 3 → F)
  (0 : Fin 3 → F)
Tactic: rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
inr :
  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)
      ⋯ =
    cross (mk F w hw) (mk F v hv)
inr₁ :
  Eq (α := ℙ 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)
        ⋯ :
      ℙ F (Fin 3 → F))
    (mk 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)
        ⋯ :
      ℙ F (Fin 3 → F))
inr₂ :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
inr₃ :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
⊢ cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
have inr₄ : Eq (α := Fin 3 → F)
  (-(((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
    Fin 3 → F)
  (0 : Fin 3 → F)
Tactic: rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
inr :
  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)
      ⋯ =
    cross (mk F w hw) (mk F v hv)
inr₁ :
  Eq (α := ℙ 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)
        ⋯ :
      ℙ F (Fin 3 → F))
    (mk 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)
        ⋯ :
      ℙ F (Fin 3 → F))
inr₂ :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
inr₃ :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
inr₄ :
  Eq (α := Fin 3 → F)
    (-(((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
⊢ cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
have inr₅ : Eq.{u_1 + 1} (α := Fin 3 → F) (-0) 0
Tactic: rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
inr :
  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)
      ⋯ =
    cross (mk F w hw) (mk F v hv)
inr₁ :
  Eq (α := ℙ 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)
        ⋯ :
      ℙ F (Fin 3 → F))
    (mk 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)
        ⋯ :
      ℙ F (Fin 3 → F))
inr₂ :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
inr₃ :
  Eq (α := Fin 3 → F)
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
inr₄ :
  Eq (α := Fin 3 → F)
    (-(((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] 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) →ₗ[F] Fin 3 → F) :
            (a : Fin 3 → F) → 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) :
      Fin 3 → F)
    (0 : Fin 3 → F)
inr₅ : Eq.{u_1 + 1} (α := Fin 3 → F) (-0) 0
⊢ cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
have inr₆ : Eq.{u_1 + 1} (α := Fin 3 → F) 0 0
Tactic: rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
w : ℙ F (Fin 3 → F)
v : Fin 3 → F
hv : v ≠ 0
h : mk F v hv ≠ w
⊢ cross (mk F v hv) w = w.cross (mk F v hv)
have inr : ∀ (w : Fin 3 → F) (hw : w ≠ 0) (h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)),
  cross (mk F v hv) (mk F w hw) = cross (mk F w hw) (mk F v hv)
Tactic: induction w with | h w hw =>
    rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
Cleared hypotheses: w, 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 : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ v.cross w = w.cross v
have inr : ∀ (v : Fin 3 → F) (hv : v ≠ 0) (h : mk F v hv ≠ w), cross (mk F v hv) w = w.cross (mk F v hv)
Tactic: induction v with | h v hv =>
    induction w with | h w hw =>
    rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]
Cleared hypotheses: v, h