awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this_1 :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this : Infinite.{u_2 + 1} (ℙ k V)
h₁ : ¬Module.Finite k V
⊢ Module.finrank k V = 0

Tactic:
apply Module.finrank_of_not_finite

Premises used: Module.finrank_of_not_finite
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this_1 :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this : Infinite.{u_2 + 1} (ℙ k V)
h₁ : ∀ (hf : Module.Finite k V), Finite V
⊢ ¬Module.Finite k V

Tactic:
contrapose hf
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this_1 :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
this : Infinite.{u_2 + 1} (ℙ k V)
hf : Module.Finite k V
⊢ Finite V

Tactic:
simpa using Module.finite_of_finite k

Premises used: Module.finite_of_finite
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this_1 :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this : Infinite.{u_2 + 1} (ℙ k V)
⊢ n = 0

Tactic:
have : n = 0 := by
      rw [← h]
      apply Module.finrank_of_not_finite
      contrapose hf
      simpa using Module.finite_of_finite k
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this_1 :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this_2 : Infinite.{u_2 + 1} (ℙ k V)
this : n = 0
⊢ Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
simp [this]
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
⊢ 1 < Nat.card k

Tactic:
have : 1 < Nat.card k := Finite.one_lt_card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
⊢ 0 < Nat.card k - 1

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
refine : Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)
⊢ Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
refine Nat.mul_right_cancel (m := Nat.card k - 1) (by lia) ?_

Premises used: Nat.mul_right_cancel
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
⊢ Module.finrank k V = Module.finrank k (Fin n → k)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
⊢ Nat.card V = Nat.card k ^ n

Tactic:
simp [Nat.card_congr e.toEquiv, Nat.card_fun]

Premises used: Nat.card_fun, Nat.card_congr, LinearEquiv.toEquiv
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
⊢ Nat.card V = Nat.card k ^ n

Tactic:
have hc : Nat.card V = Nat.card k ^ n := by simp [Nat.card_congr e.toEquiv, Nat.card_fun]
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
zify :
  HMul.hMul (α := ℤ) (↑(Nat.card.{u_2} (ℙ k V)) : ℤ) (↑(Nat.card k - 1) : ℤ) =
    HMul.hMul (α := ℤ) (∑ x ∈ Finset.range n, HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) x) (↑(Nat.card k - 1) : ℤ)
⊢ Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)

Tactic:
zify
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
rw : HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1
| HMul.hMul (α := ℤ) (∑ x ∈ Finset.range n, HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) x) (↑(Nat.card k - 1) : ℤ)

Tactic:
rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]

Premises used: LT.lt.le, geom_sum_mul, Int.natCast_sub, Int.natCast_one
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
conv_rhs :
  HMul.hMul (α := ℤ) (↑(Nat.card.{u_2} (ℙ k V)) : ℤ) (↑(Nat.card k - 1) : ℤ) =
    HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1
⊢ HMul.hMul (α := ℤ) (↑(Nat.card.{u_2} (ℙ k V)) : ℤ) (↑(Nat.card k - 1) : ℤ) =
    HMul.hMul (α := ℤ) (∑ x ∈ Finset.range n, HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) x) (↑(Nat.card k - 1) : ℤ)

Tactic:
conv_rhs => rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]

Premises used: LT.lt.le, geom_sum_mul, Int.natCast_sub, Int.natCast_one
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
rw : (↑(Nat.card k ^ n - 1) : ℤ) = HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1
⊢ HMul.hMul (α := ℤ) (↑(Nat.card.{u_2} (ℙ k V)) : ℤ) (↑(Nat.card k - 1) : ℤ) =
    HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1

Tactic:
rw [← Int.natCast_mul, ← card k V, hc]

Premises used: Projectivization.card, Int.natCast_mul
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k_1 : Type u_1
V_1 : Type u_2
inst : Field k_1
inst_1 : AddCommGroup V_1
inst_2 : Module k_1 V_1
k : Type u_1
V : Type u_2
inst_3 : Field k
inst_4 : AddCommGroup V
inst_5 : Module k V
inst_6 : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
⊢ (↑(Nat.card k ^ n - 1) : ℤ) = HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
h : Module.finrank k V = 2
⊢ Nat.card.{u_2} (ℙ k V) = Nat.card k + 1

Tactic:
simp [card_of_finrank k V h]

Premises used: Projectivization.card_of_finrank
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
x x_1 x_2 x_3 : { v : m → F // v ≠ 0 }
h : x ≈ x_2
h_1 : x_1 ≈ x_3
w : Fˣ
h1 : (fun (m_1 : Fˣ) ↦ m_1 • (↑x_2 : m → F)) w = (↑x : m → F)
w_1 : Fˣ
h2 : (fun (m_1 : Fˣ) ↦ m_1 • (↑x_3 : m → F)) w_1 = (↑x_1 : m → F)
simp_rw simp_rw₁ : ((↑x : m → F) ⬝ᵥ (↑x_1 : m → F) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
simp_rw₂ : (w • (↑x_2 : m → F) ⬝ᵥ (↑x_1 : m → F) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
simp_rw₃ : (w • (↑x_2 : m → F) ⬝ᵥ w_1 • (↑x_3 : m → F) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
simp_rw₄ : (w_1 • (w • (↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F)) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
simp_rw₅ : (w_1 • w • ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F)) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
simp_rw₆ : ((w_1 * w) • ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F)) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
⊢ Eq (α := Prop) ((fun (v w : { v : m → F // v ≠ 0 }) ↦ (↑v : m → F) ⬝ᵥ (↑w : m → F) = 0) x x_1)
    ((fun (v w : { v : m → F // v ≠ 0 }) ↦ (↑v : m → F) ⬝ᵥ (↑w : m → F) = 0) x_2 x_3)

Tactic:
simp_rw [← h1, ← h2, dotProduct_smul, smul_dotProduct, smul_smul,
      smul_eq_zero_iff_eq]

Premises used: smul_eq_zero_iff_eq, smul_smul, dotProduct_smul, smul_dotProduct
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v w : m → F
hv : v ≠ 0
hw : w ≠ 0
⊢ orthogonal (mk F v hv) (mk F w hw) ↔ v ⬝ᵥ w = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, Projectivization.orthogonal
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : w ≠ 0
h : v ⬝ᵥ w = 0 ↔ orthogonal (mk F w hw) (mk F v hv)
h₁ : v ⬝ᵥ w = 0 ↔ w ⬝ᵥ v = 0
h₂ h₃ : w ⬝ᵥ v = 0 ↔ w ⬝ᵥ v = 0
⊢ orthogonal (mk F v hv) (mk F w hw) ↔ orthogonal (mk F w hw) (mk F v hv)

Tactic:
rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]

Premises used: Projectivization.orthogonal_mk, dotProduct_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v w : ℙ F (m → F)
h : ∀ (v : m → F) (hv : v ≠ 0), orthogonal (mk F v hv) w ↔ w.orthogonal (mk F v hv)
⊢ v.orthogonal w ↔ w.orthogonal v

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

Premises used: dotProduct_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : m → F
hv : v ≠ 0
⊢ ∃ (x : m → F), ¬v ⬝ᵥ x = 0

Tactic:
rw [ne_eq, ← dotProduct_eq_zero_iff, not_forall] at hv

Premises used: ne_eq, dotProduct_eq_zero_iff, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : m → F
hv_1 : v ≠ 0
hv : ∃ (x : m → F), ¬v ⬝ᵥ x = 0
h : ∀ (w : m → F) (hw : ¬v ⬝ᵥ w = 0), ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv_1) w
⊢ ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv_1) w

Tactic:
obtain ⟨w, hw⟩ := hv
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
h : w = 0
rw : v ⬝ᵥ 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := F) 0 0
⊢ v ⬝ᵥ w = 0

Tactic:
rw [h, dotProduct_zero]

Premises used: dotProduct_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
⊢ ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv) w

Tactic:
exact ⟨mk F w fun h ↦ hw (by rw [h, dotProduct_zero]), hw⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : ℙ F (m → F)
h : ∀ (v : m → F) (hv : v ≠ 0), ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv) w
⊢ ∃ (w : ℙ F (m → F)), ¬v.orthogonal w

Tactic:
induction v with | h v hv =>
  rw [ne_eq, ← dotProduct_eq_zero_iff, not_forall] at hv
  obtain ⟨w, hw⟩ := hv
  exact ⟨mk F w fun h ↦ hw (by rw [h, dotProduct_zero]), hw⟩

Premises used: ne_eq, dotProduct_eq_zero_iff, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : ℙ F (m → F)
simp : ∃ (w : ℙ F (m → F)), ¬v.orthogonal w
⊢ ∃ (w : ℙ F (m → F)), ¬w.orthogonal v

Tactic:
simp only [orthogonal_comm]

Premises used: Projectivization.orthogonal_comm
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : ℙ F (m → F)
⊢ ∃ (w : ℙ F (m → F)), ¬v.orthogonal w

Tactic:
exists_not_self_orthogonal v

Premises used: Projectivization.exists_not_self_orthogonal
-- Module: Mathlib.LinearAlgebra.Projectivization.Constructions
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : ℙ F (m → F)
⊢ ∃ (w : ℙ F (m → F)), ¬v.orthogonal w

Tactic:
exact exists_not_self_orthogonal v

Premises used: Projectivization.exists_not_self_orthogonal
-- 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)
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
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))
        ⋯)
      (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 })
    (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)

Tactic:
split_ifs
-- 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_1 : x ≈ x_1
x_2 x_3 : { v : Fin 3 → F // v ≠ 0 }
h_2 : 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_3 :
  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ˣ
h : (fun (m : Fˣ) ↦ m • (↑x_1 : Fin 3 → F)) a = (↑x : Fin 3 → F)
⊢ x ≈ x_1

Tactic:
use a
-- 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_1 : x ≈ x_1
x_2 x_3 : { v : Fin 3 → F // v ≠ 0 }
h_2 : 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_3 :
  ¬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ˣ
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_3) :
              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))
          ⋯) :
      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))
      ⋯)
    (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_3)

Tactic:
use a * b
-- 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)
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 ⋯))
    (mk F v hv)
⊢ 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:
simp only [h]