awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
simp_rw : ¬Collinear k (P := P) ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ Set.range ![]))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
simp_rw₁ : ¬Collinear k (P := P) ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ ∅))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
simp_rw₂ : ¬Collinear k (P := P) (insert p₁ (insert p₂ (insert p₃ ∅))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
⊢ ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
simp_rw [Matrix.range_cons, Matrix.range_empty, Set.singleton_union, insert_empty_eq]

Premises used: Matrix.range_cons, Set.singleton_union, Matrix.range_empty, LawfulSingleton.insert_empty_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
⊢ Collinear k (P := P) {p₁, p₂, p₃} ↔ ¬AffineIndependent k ![p₁, p₂, p₃]

Tactic:
affineIndependent_iff_not_collinear_set.not_left.symm

Premises used: affineIndependent_iff_not_collinear_set, Iff.not_left, Iff.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}

Tactic:
decide +revert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}

Tactic:
have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by decide +revert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₃ : ¬Collinear k (p '' (↑{i₁, i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₄ : ¬Collinear k (p '' insert i₁ (↑{i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₅ : ¬Collinear k (p '' insert i₁ (insert i₂ (↑{i₃} : Set (Fin 3)))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₆ : ¬Collinear k (p '' {i₁, i₂, i₃}) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₇ : ¬Collinear k (insert (p i₁) (p '' {i₂, i₃})) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₈ rw₉ : ¬Collinear k (P := P) {p i₁, p i₂, p i₃} ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}

Tactic:
rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]

Premises used: Set.image_univ, Finset.coe_singleton, Set.image_pair, Finset.coe_univ, affineIndependent_iff_not_collinear, Set.image_insert_eq, Finset.coe_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Collinear k (P := P) {p i₁, p i₂, p i₃} ↔ ¬AffineIndependent k p

Tactic:
(affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃).not_left.symm

Premises used: affineIndependent_iff_not_collinear_of_ne, Iff.not_left, Iff.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
h : ¬Collinear k (P := P) {p₁, p₁, p₃}
⊢ False

Tactic:
simp [collinear_pair] at h

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
h : ¬Collinear k (P := P) {p₁, p₂, p₁}
⊢ False

Tactic:
simp [collinear_pair] at h

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
h : ¬Collinear k (P := P) {p₁, p₂, p₂}
⊢ False

Tactic:
simp [collinear_pair] at h

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
rw :
  ∀ (h : ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) {p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s)
    (hp₁p₂ : p₁ ≠ p₂), Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃

Tactic:
rw [collinear_iff_of_mem hp₁] at h

Premises used: collinear_iff_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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 : ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
rcases :
  ∀ (v : V) (h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃

Tactic:
rcases h with ⟨v, h⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
rcases :
  ∀ (r₂ : k) (hp₂ : r₂ • v +ᵥ p₁ ∈ s) (hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) p₃
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃

Tactic:
rcases h p₂ hp₂ with ⟨r₂, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃ : P
hp₁ : p₁ ∈ s
hp₃ : p₃ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
rcases :
  ∀ (r₃ : k) (hp₃ : r₃ • v +ᵥ p₁ ∈ s),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) (r₃ • v +ᵥ p₁)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) p₃

Tactic:
rcases h p₃ hp₃ with ⟨r₃, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
rw : ∃ (r : k), r • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) (r₃ • v +ᵥ p₁)

Tactic:
rw [vadd_left_mem_affineSpan_pair]

Premises used: vadd_left_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ ∃ (r : k), r • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v

Tactic:
⟨r₃ / r₂, ?_⟩

Premises used: HDiv.hDiv, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
refine : (r₃ / r₂) • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v
⊢ ∃ (r : k), r • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v

Tactic:
refine ⟨r₃ / r₂, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
hp₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v +ᵥ p₁
⊢ False

Tactic:
simp at hp₁p₂
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ r₂ ≠ 0

Tactic:
have h₂ : r₂ ≠ 0 := by
    rintro rfl
    simp at hp₁p₂
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
h₂ : r₂ ≠ 0
⊢ (r₃ / r₂) • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v

Tactic:
simp [smul_smul, h₂]

Premises used: smul_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ Eq (α := AffineSubspace k P) (affineSpan k {p₁, p₂}) (affineSpan k s)

Tactic:
le_antisymm (affineSpan_mono _ (Set.insert_subset_iff.2 ⟨hp₁, Set.singleton_subset_iff.2 hp₂⟩))
    (affineSpan_le.2 fun _ hp => h.mem_affineSpan_of_mem_of_ne hp₁ hp₂ hp hp₁p₂)

Premises used: Iff.mpr, Set.singleton_subset_iff, Collinear.mem_affineSpan_of_mem_of_ne, affineSpan_le, Set.insert_subset_iff, le_antisymm, And.intro, affineSpan_mono
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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 : direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P)))
| vectorSpan k (P := P) {p₁, p₂, p₃}

Tactic:
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]

Premises used: direction_affineSpan, affineSpan_insert_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃
conv_rhs :
  Eq (α := Submodule k V) (vectorSpan k (insert p₁ s))
    (direction (affineSpan k (insert p₁ (↑(affineSpan k {p₂, p₃}) : Set P))))
⊢ Eq (α := Submodule k V) (vectorSpan k (insert p₁ s)) (vectorSpan k (P := P) {p₁, p₂, p₃})

Tactic:
conv_rhs => rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]

Premises used: direction_affineSpan, affineSpan_insert_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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))))
rw₂ 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))))
⊢ Eq (α := Submodule k V) (vectorSpan 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₃]

Premises used: direction_affineSpan, Collinear.affineSpan_eq_of_ne, affineSpan_insert_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃})

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₃]
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
rw₂ rw₃ :
  Module.rank k ↥(vectorSpan k (P := P) {p₁, p₂, p₃}) ≤ 1 ↔ Module.rank k ↥(vectorSpan k (P := P) {p₁, p₂, p₃}) ≤ 1
⊢ Collinear k (insert p₁ s) ↔ Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
rw [Collinear, Collinear, hv]

Premises used: Collinear
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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
rw₂ rw₃ : Module.rank k ↥(vectorSpan k s) ≤ 1 ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k (insert p s) ↔ Collinear k s

Tactic:
rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]

Premises used: Collinear, vectorSpan_insert_eq_vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₁
rw : Collinear k (P := P) {p₂, p₃}
⊢ Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
rw [collinear_insert_iff_of_mem_affineSpan h]

Premises used: collinear_insert_iff_of_mem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃}

Tactic:
collinear_pair _ _ _

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃}

Tactic:
exact collinear_pair _ _ _

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₂
rw : Collinear k (P := P) {p₃, p₄}
⊢ Collinear k (P := P) {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₂]

Premises used: AffineSubspace.le_def', Iff.mp, collinear_insert_iff_of_mem_affineSpan, affineSpan_mono, Set.subset_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₄}

Tactic:
collinear_pair _ _ _

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₄}

Tactic:
exact collinear_pair _ _ _

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃
rw : Collinear k (P := P) {p₄, p₅}
⊢ Collinear k (P := P) {p₁, 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₃]

Premises used: AffineSubspace.le_def', HasSubset.Subset.trans, Iff.mp, collinear_insert_iff_of_mem_affineSpan, affineSpan_mono, Set.subset_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₅}

Tactic:
collinear_pair _ _ _

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₅}

Tactic:
exact collinear_pair _ _ _

Premises used: collinear_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₄}

Tactic:
(collinear_insert_insert_insert_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_

Premises used: collinear_insert_insert_insert_of_mem_affineSpan_pair, Collinear.subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃
refine : Subset (α := Set P) {p₁, p₂, p₃, p₄} {p₁, p₂, p₃, p₄, p₅}
⊢ Collinear k (P := P) {p₁, p₂, p₃, p₄}

Tactic:
refine (collinear_insert_insert_insert_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_

Premises used: collinear_insert_insert_insert_of_mem_affineSpan_pair, Collinear.subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃
h : Subset (α := Set P) {p₄} {p₄, p₅}
⊢ Subset (α := Set P) {p₁, p₂, p₃, p₄} {p₁, p₂, p₃, p₄, p₅}

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₅}

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃}

Tactic:
(collinear_insert_insert_insert_left_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_

Premises used: collinear_insert_insert_insert_left_of_mem_affineSpan_pair, Collinear.subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
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₃
refine : Subset (α := Set P) {p₁, p₂, p₃} {p₁, p₂, p₃, p₄}
⊢ Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
refine (collinear_insert_insert_insert_left_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_

Premises used: collinear_insert_insert_insert_left_of_mem_affineSpan_pair, Collinear.subset