awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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)
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)
            ⋯) :
      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))
⊢ 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:
simp only [h]
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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''
      (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 ⋯))
    (mk F v hv)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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''
        (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)
            ⋯) :
      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:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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)
rw₁ rw₂ : Eq (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F v hv)
⊢ Eq (α := ℙ F (Fin 3 → F)) (cross (mk F v hv) (mk F w hw)) (mk F v hv)

Tactic:
rw [cross_mk, dif_pos h]

Premises used: dif_pos, Projectivization.cross_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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))
rw₁ 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))
⊢ 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)

Tactic:
rw [cross_mk, dif_neg h]

Premises used: dif_neg, Projectivization.cross_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 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)
        v :
      Fin 3 → F)
    (0 : Fin 3 → F)
⊢ cross (mk F v hv) (mk F v hv) = mk F v hv

Tactic:
rw [cross_mk_of_cross_eq_zero]

Premises used: Projectivization.cross_mk_of_cross_eq_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
h : Eq (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F v hv)
h₁ : v ≠ 0
h₂ : Eq (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F v hv)
h₃ : 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)

Tactic:
rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]

Premises used: Projectivization.mk_eq_mk_iff_crossProduct_eq_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : ℙ F (Fin 3 → F)
h : ∀ (v : Fin 3 → F) (hv : v ≠ 0), cross (mk F v hv) (mk F v hv) = mk F v hv
⊢ v.cross v = v

Tactic:
induction v with | h v hv =>
  rw [cross_mk_of_cross_eq_zero]
  rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]

Premises used: Projectivization.cross_mk_of_cross_eq_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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))
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))
    (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))
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)
      ⋯)

Tactic:
rw [cross_mk_of_cross_ne_zero]

Premises used: Projectivization.cross_mk_of_cross_ne_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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
inr : ∀ (h : v ≠ w), v.cross w = w.cross v
⊢ v.cross w = w.cross v

Tactic:
rcases eq_or_ne v w with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v.cross v

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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
inr₆ 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)

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]

Premises used: cross_self, cross_anticomm, Ne.symm, map_neg, Projectivization.mk_eq_mk_iff_crossProduct_eq_zero, Projectivization.cross_mk_of_ne, neg_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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
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)
⊢ cross (mk F v hv) w = w.cross (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]

Premises used: cross_self, map_neg, Projectivization.mk_eq_mk_iff_crossProduct_eq_zero, neg_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
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)
⊢ v.cross w = w.cross v

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]

Premises used: cross_self, cross_anticomm, map_neg, Projectivization.mk_eq_mk_iff_crossProduct_eq_zero, neg_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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)
h₁ :
  orthogonal
    (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)
      ⋯)
    (mk F v hv)
h₂ :
  (((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 ⬝ᵥ
      v =
    0
h₃ :
  v ⬝ᵥ
      (((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 =
    0
h₄ h₅ : Eq.{u_1 + 1} (α := F) 0 0
⊢ (cross (mk F v hv) (mk F w hw)).orthogonal (mk F v hv)

Tactic:
rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Premises used: dot_self_cross, Projectivization.orthogonal_mk, Projectivization.cross_mk_of_ne, dotProduct_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
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
h₁ :
  ∀ (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)).orthogonal (mk F v hv)
⊢ (cross (mk F v hv) w).orthogonal (mk F v hv)

Tactic:
induction w with | h w hw =>
  rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Premises used: dot_self_cross, Projectivization.orthogonal_mk, dotProduct_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
h₁ : ∀ (v : Fin 3 → F) (hv : v ≠ 0) (h : mk F v hv ≠ w), (cross (mk F v hv) w).orthogonal (mk F v hv)
⊢ (v.cross w).orthogonal v

Tactic:
induction v with | h v hv =>
  induction w with | h w hw =>
  rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Premises used: dot_self_cross, Projectivization.orthogonal_mk, dotProduct_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
rw : (w.cross v).orthogonal w
⊢ (v.cross w).orthogonal w

Tactic:
rw [cross_comm]

Premises used: Projectivization.cross_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (w.cross v).orthogonal w

Tactic:
cross_orthogonal_left h.symm

Premises used: Projectivization.cross_orthogonal_left, Ne.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (w.cross v).orthogonal w

Tactic:
exact cross_orthogonal_left h.symm

Premises used: Projectivization.cross_orthogonal_left, Ne.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
rw : (v.cross w).orthogonal v
⊢ v.orthogonal (v.cross w)

Tactic:
rw [orthogonal_comm]

Premises used: Projectivization.orthogonal_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v

Tactic:
cross_orthogonal_left h

Premises used: Projectivization.cross_orthogonal_left
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v

Tactic:
exact cross_orthogonal_left h

Premises used: Projectivization.cross_orthogonal_left
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
rw : (v.cross w).orthogonal w
⊢ w.orthogonal (v.cross w)

Tactic:
rw [orthogonal_comm]

Premises used: Projectivization.orthogonal_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal w

Tactic:
cross_orthogonal_right h

Premises used: Projectivization.cross_orthogonal_right
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal w

Tactic:
exact cross_orthogonal_right h

Premises used: Projectivization.cross_orthogonal_right
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)

Tactic:
⟨?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
refine_1 : Independent f → LinearIndependent K (Projectivization.rep ∘ f)
refine_2 : ∀ (h : LinearIndependent K (Projectivization.rep ∘ f)), Independent f
⊢ Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)

Tactic:
refine ⟨?_, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
refine_1 :
  ∀ (a : (i : ι) → Kˣ) (ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)),
    LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
      (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
⊢ LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)

Tactic:
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)

Premises used: Projectivization.exists_smul_eq_mk_rep
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
⊢ LinearIndependent K (a • ff)

Tactic:
hh.units_smul a

Premises used: LinearIndependent.units_smul
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
h : (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯) = a • ff
⊢ LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)

Tactic:
convert! hh.units_smul a

Premises used: LinearIndependent.units_smul
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
h : ∀ (i : ι), Function.comp (β := ℙ K V) Projectivization.rep (fun (i : ι) ↦ mk K (ff i) ⋯) i = (a • ff) i
⊢ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯) = a • ff

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
i : ι
⊢ Function.comp (β := ℙ K V) Projectivization.rep (fun (i : ι) ↦ mk K (ff i) ⋯) i = (a • ff) i

Tactic:
(ha i).symm

Premises used: Projectivization.rep, Eq.symm