awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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 :
  ∀ (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
⊢ Infinite.{u_2 + 1} (ℙ k V)
have contrapose! : ∀ (hf : Finite.{u_2 + 1} (ℙ k V)), Finite V
Tactic: contrapose! hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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 :
  ∀ (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.{u_2 + 1} (ℙ k V)
⊢ Finite V
have rwa : ∀ (hf : Finite V), Finite V
Tactic: rwa [finite_iff_of_finite] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (hypothesis)
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 :
  ∀ (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
⊢ Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
have this₁ : Infinite.{u_2 + 1} (ℙ k V)
Tactic: have : Infinite (ℙ k V) := by
      contrapose! hf
      rwa [finite_iff_of_finite] at hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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
have rw : Module.finrank k V = 0
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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)
⊢ Module.finrank k V = 0
have h₁ : ¬Module.Finite k V
Tactic: apply Module.finrank_of_not_finite
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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)
⊢ ¬Module.Finite k V
have h₁ : ∀ (hf : Module.Finite k V), Finite V
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (hypothesis)
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)
⊢ Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
have this₁ : n = 0
Tactic: have : n = 0 := by
      rw [← h]
      apply Module.finrank_of_not_finite
      contrapose hf
      simpa using Module.finite_of_finite k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (hypothesis)
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
⊢ Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
have this : 1 < Nat.card k
Tactic: have : 1 < Nat.card k := Finite.one_lt_card
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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
⊢ Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
have refine : Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)
Tactic: refine Nat.mul_right_cancel (m := Nat.card k - 1) (by lia) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (hypothesis)
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.{u_2} (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)
have hc : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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.{u_2} (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)
have 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) : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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
| HMul.hMul (α := ℤ) (∑ x ∈ Finset.range n, HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) x) (↑(Nat.card k - 1) : ℤ)
have rw : HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1
Tactic: rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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
⊢ 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) : ℤ)
have conv_rhs : HMul.hMul (α := ℤ) (↑(Nat.card.{u_2} (ℙ k V)) : ℤ) (↑(Nat.card k - 1) : ℤ) =
  HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1
Tactic: conv_rhs => rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Cardinality (goal)
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
⊢ HMul.hMul (α := ℤ) (↑(Nat.card.{u_2} (ℙ k V)) : ℤ) (↑(Nat.card k - 1) : ℤ) =
    HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1
have rw : (↑(Nat.card k ^ n - 1) : ℤ) = HPow.hPow (α := ℤ) (↑(Nat.card k) : ℤ) n - 1
Tactic: rw [← Int.natCast_mul, ← card k V, hc]
-- 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
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)
⊢ 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)
have simp_rw₂ : (w • (↑x_2 : m → F) ⬝ᵥ (↑x_1 : m → F) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
Tactic: simp_rw [← h1, ← h2, dotProduct_smul, smul_dotProduct, smul_smul,
      smul_eq_zero_iff_eq]
-- 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
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)
⊢ 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)
have simp_rw₃ : (w • (↑x_2 : m → F) ⬝ᵥ w_1 • (↑x_3 : m → F) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
Tactic: simp_rw [← h1, ← h2, dotProduct_smul, smul_dotProduct, smul_smul,
      smul_eq_zero_iff_eq]
-- 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
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)
⊢ 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)
have simp_rw₄ : (w_1 • (w • (↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F)) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
Tactic: simp_rw [← h1, ← h2, dotProduct_smul, smul_dotProduct, smul_smul,
      smul_eq_zero_iff_eq]
-- 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
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)
⊢ 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)
have simp_rw₅ : (w_1 • w • ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F)) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
Tactic: simp_rw [← h1, ← h2, dotProduct_smul, smul_dotProduct, smul_smul,
      smul_eq_zero_iff_eq]
-- 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
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)
⊢ 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)
have simp_rw₆ : ((w_1 * w) • ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F)) = 0) = ((↑x_2 : m → F) ⬝ᵥ (↑x_3 : m → F) = 0)
Tactic: simp_rw [← h1, ← h2, dotProduct_smul, smul_dotProduct, smul_smul,
      smul_eq_zero_iff_eq]
-- 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
v : m → F
hv : v ≠ 0
w : m → F
hw : w ≠ 0
⊢ orthogonal (mk F v hv) (mk F w hw) ↔ orthogonal (mk F w hw) (mk F v hv)
have h : v ⬝ᵥ w = 0 ↔ orthogonal (mk F w hw) (mk F v hv)
Tactic: rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]
-- 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
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)
⊢ orthogonal (mk F v hv) (mk F w hw) ↔ orthogonal (mk F w hw) (mk F v hv)
have h₁ : v ⬝ᵥ w = 0 ↔ w ⬝ᵥ v = 0
Tactic: rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]
-- 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
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
⊢ orthogonal (mk F v hv) (mk F w hw) ↔ orthogonal (mk F w hw) (mk F v hv)
have h₂ : w ⬝ᵥ v = 0 ↔ w ⬝ᵥ v = 0
Tactic: rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]
-- 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
v w : ℙ F (m → F)
⊢ v.orthogonal w ↔ w.orthogonal v
have h : ∀ (v : m → F) (hv : v ≠ 0), orthogonal (mk F v hv) w ↔ w.orthogonal (mk F v hv)
Tactic: induction v with | h v hv => induction w with | h w hw =>
  rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (hypothesis)
Goal:
F : Type u_1
inst : Field F
m : Type u_2
inst_1 : Fintype m
v : m → F
hv : v ≠ 0
⊢ ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv) w
have hv₁ : ∃ (x : m → F), ¬v ⬝ᵥ x = 0
Tactic: rw [ne_eq, ← dotProduct_eq_zero_iff, not_forall] at hv
-- 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
v : m → F
hv_1 : v ≠ 0
hv : ∃ (x : m → F), ¬v ⬝ᵥ x = 0
⊢ ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv_1) w
have h : ∀ (w : m → F) (hw : ¬v ⬝ᵥ w = 0), ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv_1) w
Tactic: obtain ⟨w, hw⟩ := hv
Cleared hypotheses: hv
-- 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
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
h : w = 0
⊢ v ⬝ᵥ w = 0
have rw : v ⬝ᵥ 0 = 0
Tactic: rw [h, dotProduct_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
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
h : w = 0
rw : v ⬝ᵥ 0 = 0
⊢ v ⬝ᵥ w = 0
have rw₁ : Eq.{u_1 + 1} (α := F) 0 0
Tactic: rw [h, dotProduct_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
v : ℙ F (m → F)
⊢ ∃ (w : ℙ F (m → F)), ¬v.orthogonal w
have h : ∀ (v : m → F) (hv : v ≠ 0), ∃ (w : ℙ F (m → F)), ¬orthogonal (mk F v hv) 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⟩
Cleared hypotheses: v
-- 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
v : ℙ F (m → F)
⊢ ∃ (w : ℙ F (m → F)), ¬w.orthogonal v
have simp : ∃ (w : ℙ F (m → F)), ¬v.orthogonal w
Tactic: simp only [orthogonal_comm]
-- 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
⊢ 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 : ¬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)
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)
⊢ 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₁ : (¬∃ (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)
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)
⊢ 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₂ : (∀ (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)
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)
⊢ 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₃ : 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)
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]