awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
| vectorSpan k (P := P) {p₁, p₂, p₃}
have rw : direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P)))
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ Eq (α := Submodule k V) (vectorSpan k (insert p₁ s)) (vectorSpan k (P := P) {p₁, p₂, p₃})
have conv_rhs : Eq (α := Submodule k V) (vectorSpan k (insert p₁ s))
  (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
Tactic: conv_rhs => rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ Eq (α := Submodule k V) (vectorSpan k (insert p₁ s))
    (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
have rw : Eq (α := Submodule k V) (direction (affineSpan k (insert p₁ s)))
  (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
rw :
  Eq (α := Submodule k V) (direction (affineSpan k (insert p₁ s)))
    (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
⊢ Eq (α := Submodule k V) (vectorSpan k (insert p₁ s))
    (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
have rw₁ : Eq (α := Submodule k V) (direction (affineSpan k (insert p₁ (↑(affineSpan k s) : Set P))))
  (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
rw :
  Eq (α := Submodule k V) (direction (affineSpan k (insert p₁ s)))
    (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
rw₁ :
  Eq (α := Submodule k V) (direction (affineSpan k (insert p₁ (↑(affineSpan k s) : Set P))))
    (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
⊢ Eq (α := Submodule k V) (vectorSpan k (insert p₁ s))
    (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
have rw₂ : Eq (α := Submodule k V) (direction (affineSpan k (insert p₁ (↑(affineSpan k s) : Set P))))
  (direction (affineSpan k (insert p₁ (↑(affineSpan k s) : Set P))))
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ Collinear k (insert p₁ s) ↔ Collinear k (P := P) {p₁, p₂, p₃}
have hv : Eq (α := Submodule k V) (vectorSpan k (insert p₁ s)) (vectorSpan k (P := P) {p₁, p₂, p₃})
Tactic: have hv : vectorSpan k (insert p₁ s) = vectorSpan k ({p₁, p₂, p₃} : Set P) := by
    conv_rhs => rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
    rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : Eq (α := Submodule k V) (vectorSpan k (insert p₁ s)) (vectorSpan k (P := P) {p₁, p₂, p₃})
⊢ Collinear k (insert p₁ s) ↔ Collinear k (P := P) {p₁, p₂, p₃}
have rw : Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Collinear k (P := P) {p₁, p₂, p₃}
Tactic: rw [Collinear, Collinear, hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : Eq (α := Submodule k V) (vectorSpan k (insert p₁ s)) (vectorSpan k (P := P) {p₁, p₂, p₃})
rw : Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Collinear k (P := P) {p₁, p₂, p₃}
⊢ Collinear k (insert p₁ s) ↔ Collinear k (P := P) {p₁, p₂, p₃}
have rw₁ : Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Module.rank k ↥(vectorSpan k (P := P) {p₁, p₂, p₃}) ≤ 1
Tactic: rw [Collinear, Collinear, hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : Eq (α := Submodule k V) (vectorSpan k (insert p₁ s)) (vectorSpan k (P := P) {p₁, p₂, p₃})
rw : Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Collinear k (P := P) {p₁, p₂, p₃}
rw₁ : Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Module.rank k ↥(vectorSpan k (P := P) {p₁, p₂, p₃}) ≤ 1
⊢ Collinear k (insert p₁ s) ↔ Collinear k (P := P) {p₁, p₂, p₃}
have rw₂ : Module.rank k ↥(vectorSpan k (P := P) {p₁, p₂, p₃}) ≤ 1 ↔ Module.rank k ↥(vectorSpan k (P := P) {p₁, p₂, p₃}) ≤ 1
Tactic: rw [Collinear, Collinear, hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
⊢ Collinear k (insert p s) ↔ Collinear k s
have rw : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Collinear k s
Tactic: rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
rw : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Collinear k s
⊢ Collinear k (insert p s) ↔ Collinear k s
have rw₁ : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
Tactic: rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
rw : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Collinear k s
rw₁ : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k (insert p s) ↔ Collinear k s
have rw₂ : Module.rank k ↥(vectorSpan k s) ≤ 1 ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
Tactic: rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p₃}) p₁
⊢ Collinear k (P := P) {p₁, p₂, p₃}
have rw : Collinear k (P := P) {p₂, p₃}
Tactic: rw [collinear_insert_iff_of_mem_affineSpan h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₂
⊢ Collinear k (P := P) {p₁, p₂, p₃, p₄}
have rw : Collinear k (P := P) {p₃, p₄}
Tactic: rw [collinear_insert_iff_of_mem_affineSpan
      ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k (Set.subset_insert _ _)) _ h₁),
    collinear_insert_iff_of_mem_affineSpan h₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₂
h₃ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₃
⊢ Collinear k (P := P) {p₁, p₂, p₃, p₄, p₅}
have rw : Collinear k (P := P) {p₄, p₅}
Tactic: rw [collinear_insert_iff_of_mem_affineSpan
      ((AffineSubspace.le_def' _ _).1
        (affineSpan_mono k ((Set.subset_insert _ _).trans (Set.subset_insert _ _))) _ h₁),
    collinear_insert_iff_of_mem_affineSpan
      ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k (Set.subset_insert _ _)) _ h₂),
    collinear_insert_iff_of_mem_affineSpan h₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₂
h₃ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₃
⊢ Collinear k (P := P) {p₁, p₂, p₃, p₄}
have refine : Subset (α := Set P) {p₁, p₂, p₃, p₄} {p₁, p₂, p₃, p₄, p₅}
Tactic: refine (collinear_insert_insert_insert_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₂
h₃ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₃
⊢ Subset (α := Set P) {p₁, p₂, p₃, p₄} {p₁, p₂, p₃, p₄, p₅}
have h : Subset (α := Set P) {p₄} {p₄, p₅}
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₂
h₃ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₃
⊢ Collinear k (P := P) {p₁, p₂, p₃}
have refine : Subset (α := Set P) {p₁, p₂, p₃} {p₁, p₂, p₃, p₄}
Tactic: refine (collinear_insert_insert_insert_left_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₂
h₃ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₃
⊢ Subset (α := Set P) {p₁, p₂, p₃} {p₁, p₂, p₃, p₄}
have h : Subset (α := Set P) {p₃} {p₃, p₄}
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
⊢ AffineIndependent k ![p₁, p₂, p]
have rw : ¬Collinear k (P := P) {p₁, p₂, p}
Tactic: rw [affineIndependent_iff_not_collinear_set]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Collinear k (P := P) {p₁, p₃, p₂, p}
have h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p}) p₁
Tactic: apply collinear_insert_insert_of_mem_affineSpan_pair
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p}) p₁
⊢ Collinear k (P := P) {p₁, p₃, p₂, p}
have h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p}) p₃
Tactic: apply collinear_insert_insert_of_mem_affineSpan_pair
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ False
have h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
Tactic: have h1 : Collinear k {p₁, p₃, p₂, p} := by
    apply collinear_insert_insert_of_mem_affineSpan_pair
    · apply Collinear.mem_affineSpan_of_mem_of_ne h (by simp) (by simp) (by simp) hne
    · apply Collinear.mem_affineSpan_of_mem_of_ne hcol (by simp) (by simp) (by simp) hne
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
⊢ False
have h2 : Collinear k (P := P) {p₁, p₂, p₃}
Tactic: have h2 : Collinear k {p₁, p₂, p₃} := h1.subset (by grind)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
⊢ False
have ha₁ : ¬Collinear k (P := P) {p₁, p₂, p₃}
Tactic: rw [affineIndependent_iff_not_collinear_set] at ha
Cleared hypotheses: ha, hcol, hne, h, h1, h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k (P := P) {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
⊢ AffineIndependent k ![p₁, p₂, p] ↔ AffineIndependent k ![p₁, p₂, p₃]
have refine : ∀ (h : AffineIndependent k ![p₁, p₂, p₃]), Collinear k (P := P) {p₂, p₃, p}
Tactic: refine ⟨fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h hcol hne2,
    fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h ?_ hne1⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k (P := P) {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ Collinear k (P := P) {p₂, p₃, p}
have h₁ : Eq (α := Set P) {p₂, p₃, p} {p₂, p, p₃}
Tactic: convert! hcol using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
have refine : 2 < Cardinal.aleph0
Tactic: refine IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h ?_))
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
⊢ Coplanar k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 2
have h : Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
Tactic: have h : Coplanar k s ↔ Module.rank k (vectorSpan k s) ≤ 2 := Iff.rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 2
have h₁ : Coplanar k s ↔ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} k ↥(vectorSpan k s)) : Cardinal.{u_2}) 2
Tactic: rw [← finrank_eq_rank] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
⊢ Coplanar k (insert p s) ↔ Coplanar k s
have rw : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Coplanar k s
Tactic: rw [Coplanar, Coplanar, vectorSpan_insert_eq_vectorSpan h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
rw : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Coplanar k s
⊢ Coplanar k (insert p s) ↔ Coplanar k s
have rw₁ : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
Tactic: rw [Coplanar, Coplanar, vectorSpan_insert_eq_vectorSpan h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
rw : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Coplanar k s
rw₁ : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k (insert p s) ↔ Coplanar k s
have rw₂ : Module.rank k ↥(vectorSpan k s) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
Tactic: rw [Coplanar, Coplanar, vectorSpan_insert_eq_vectorSpan h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
have pos : ∀ (hf : FiniteDimensional.{u_1, u_2} k ↥s.direction),
  finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
Tactic: by_cases hf : FiniteDimensional k s.direction
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
pos :
  ∀ (hf : FiniteDimensional.{u_1, u_2} k ↥s.direction),
    finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
have neg : ∀ (hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction),
  finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
Tactic: by_cases hf : FiniteDimensional k s.direction
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction
h : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P)))
⊢ False
have h' : s.direction ≤ vectorSpan k (insert p (↑s : Set P))
Tactic: have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
        conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
        exact vectorSpan_mono k (Set.subset_insert _ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
have hf' : ¬FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P)))
Tactic: have hf' : ¬FiniteDimensional k (vectorSpan k (insert p (s : Set P))) := by
      intro h
      have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
        conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
        exact vectorSpan_mono k (Set.subset_insert _ _)
      exact hf (Submodule.finiteDimensional_of_le h')
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction
hf' : ¬FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P)))
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
have neg : LE.le (α := ℕ) 0 1
Tactic: rw [finrank_of_infinite_dimensional hf, finrank_of_infinite_dimensional hf', zero_add]