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
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k s ↔ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} k ↥(vectorSpan k s)) : Cardinal.{u_2}) 1

Tactic:
rw [← finrank_eq_rank] at h

Premises used: Module.finrank_eq_rank
-- 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
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Collinear k s ↔ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} k ↥(vectorSpan k s)) : Cardinal.{u_2}) 1
⊢ Collinear k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 1

Tactic:
mod_cast h

Premises used: Collinear, vectorSpan, congrArg, cast, Membership.mem, Subtype, Nat.cast_le._simp_1, LE.le, Nat.cast, Iff, Eq.symm, Nat.cast_one, Module.finrank, Eq.trans
-- 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
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Collinear k s ↔ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} k ↥(vectorSpan k s)) : Cardinal.{u_2}) 1
⊢ Collinear k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 1

Tactic:
exact mod_cast 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₁ s₂ : Set P
hs : s₁ ⊆ s₂
h : Collinear k s₂
⊢ Collinear k s₁

Tactic:
(Submodule.rank_mono (vectorSpan_mono k hs)).trans h

Premises used: Collinear, Submodule.rank_mono, vectorSpan_mono, LE.le.trans
-- 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
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)

Tactic:
IsNoetherian.iff_fg.1
    (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h Cardinal.one_lt_aleph0))

Premises used: Iff.mpr, IsNoetherian.iff_rank_lt_aleph0, lt_of_le_of_lt, Cardinal.one_lt_aleph0, IsNoetherian.iff_fg, Iff.mp
-- 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
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))

Tactic:
(direction_affineSpan k s).symm ▸ h.finiteDimensional_vectorSpan

Premises used: direction_affineSpan, Eq.rec, Collinear.finiteDimensional_vectorSpan, Eq.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
rw : Module.rank k ↥⊥ ≤ 1
⊢ Collinear.{u_1, u_2, u_3} k (P := P) ∅

Tactic:
rw [collinear_iff_rank_le_one, vectorSpan_empty]

Premises used: vectorSpan_empty, collinear_iff_rank_le_one
-- 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
⊢ Module.rank k ↥⊥ ≤ 1

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
rw : Module.rank k ↥⊥ ≤ 1
⊢ Collinear k (P := P) {p}

Tactic:
rw [collinear_iff_rank_le_one, vectorSpan_singleton]

Premises used: collinear_iff_rank_le_one, vectorSpan_singleton
-- 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
⊢ Module.rank k ↥⊥ ≤ 1

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
s : Set P
p₀ : P
h : p₀ ∈ s
simp_rw :
  (∃ (v₀ : V), ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v) ↔
    ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
⊢ Collinear k s ↔ ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
simp_rw [collinear_iff_rank_le_one, rank_submodule_le_one_iff', Submodule.le_span_singleton_iff]

Premises used: rank_submodule_le_one_iff', Submodule.le_span_singleton_iff, collinear_iff_rank_le_one
-- 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 : p₀ ∈ s
mp :
  (∃ (v₀ : V), ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v) →
    ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
mpr :
  (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀) →
    ∃ (v₀ : V), ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v
⊢ (∃ (v₀ : V), ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v) ↔
    ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
constructor
-- 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 : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v
h₁ : ∀ p ∈ s, ∃ (r : k), p = r • v₀ +ᵥ p₀
⊢ ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
use v₀
-- 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 : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v
p : P
hp : p ∈ s
h₁ : ∀ (r : k) (hr : r • v₀ = p -ᵥ p₀), ∃ (r : k), p = r • v₀ +ᵥ p₀
⊢ ∃ (r : k), p = r • v₀ +ᵥ p₀

Tactic:
obtain ⟨r, hr⟩ := hv (p -ᵥ p₀) (vsub_mem_vectorSpan k hp h)

Premises used: vsub_mem_vectorSpan, VSub.vsub
-- 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 : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
h₁ : p = r • v₀ +ᵥ p₀
⊢ ∃ (r : k), p = r • v₀ +ᵥ p₀

Tactic:
use 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
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
h₁ : p -ᵥ p₀ = r • v₀
⊢ p = r • v₀ +ᵥ p₀

Tactic:
rw [eq_vadd_iff_vsub_eq]

Premises used: eq_vadd_iff_vsub_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
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ p -ᵥ p₀ = r • v₀

Tactic:
hr.symm

Premises used: Eq.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
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ p -ᵥ p₀ = r • v₀

Tactic:
exact hr.symm

Premises used: Eq.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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
h₁ : ∀ (v_1 : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v_1 → ∃ (r : k), r • v = v_1
⊢ ∃ (v₀ : V), ∀ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v → ∃ (r : k), r • v₀ = v

Tactic:
use v
-- 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 : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
rw : ∀ (x : V), Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p₀) '' s) x → x ∈ (↑(k ∙ v) : Set V)
⊢ LE.le (α := Submodule k V) (vectorSpan k s) (k ∙ v)

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k h, Submodule.span_le, Set.subset_def]

Premises used: Set.subset_def, vectorSpan_eq_span_vsub_set_right, Submodule.span_le
-- 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 : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
x : V
hx : Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p₀) '' s) x
rw : ∃ (a : k), a • v = x
⊢ x ∈ (↑(k ∙ v) : Set V)

Tactic:
rw [SetLike.mem_coe, Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton, SetLike.mem_coe
-- 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 : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
x : V
hx : Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p₀) '' s) x
⊢ ∃ x_1 ∈ s, x_1 -ᵥ p₀ = x

Tactic:
rw [Set.mem_image] at hx

Premises used: Set.mem_image
-- 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 : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
x : V
hx : ∃ x_1 ∈ s, x_1 -ᵥ p₀ = x
rcases : ∀ (p : P) (hp : p ∈ s), ∃ (a : k), a • v = p -ᵥ p₀
⊢ ∃ (a : k), a • v = x

Tactic:
rcases hx with ⟨p, hp, 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
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
p : P
hp : p ∈ s
rcases : ∀ (r : k) (hp : r • v +ᵥ p₀ ∈ s), ∃ (a : k), a • v = (r • v +ᵥ p₀) -ᵥ p₀
⊢ ∃ (a : k), a • v = p -ᵥ p₀

Tactic:
rcases hp₀v 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
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
r : k
hp : r • v +ᵥ p₀ ∈ s
h₁ : r • v = (r • v +ᵥ p₀) -ᵥ p₀
⊢ ∃ (a : k), a • v = (r • v +ᵥ p₀) -ᵥ p₀

Tactic:
use 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
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
r : k
hp : r • v +ᵥ p₀ ∈ s
⊢ r • v = (r • v +ᵥ 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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
⊢ LE.le (α := Submodule k V) (vectorSpan k s) (k ∙ v)

Tactic:
have hs : vectorSpan k s ≤ k ∙ v := by
      rw [vectorSpan_eq_span_vsub_set_right k h, Submodule.span_le, Set.subset_def]
      intro x hx
      rw [SetLike.mem_coe, Submodule.mem_span_singleton]
      rw [Set.mem_image] at hx
      rcases hx with ⟨p, hp, rfl⟩
      rcases hp₀v p hp with ⟨r, rfl⟩
      use r
      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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
hs : LE.le (α := Submodule k V) (vectorSpan k s) (k ∙ v)
⊢ Membership.mem (γ := Submodule k V) (k ∙ v) w

Tactic:
have hw' := SetLike.le_def.1 hs hw
-- 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 : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
w : V
hw : Membership.mem (γ := Submodule k V) (vectorSpan k s) w
hs : LE.le (α := Submodule k V) (vectorSpan k s) (k ∙ v)
hw' : Membership.mem (γ := Submodule k V) (k ∙ v) w
h₁ h₂ h₃ h₄ : ∀ (hw' : ∃ (a : k), a • v = w), ∃ (r : k), r • v = w
⊢ ∃ (r : k), r • v = w

Tactic:
rwa [Submodule.mem_span_singleton] at hw'

Premises used: Submodule.mem_span_singleton
-- 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
inl :
  Collinear.{u_1, u_2, u_3} k (P := P) ∅ ↔
    ∃ (p₀ : P) (v : V), ∀ (p : P), Membership.mem (γ := Set P) ∅ p → ∃ (r : k), p = r • v +ᵥ p₀
inr : ∀ (p₁ : P) (hp₁ : p₁ ∈ s), Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
⊢ Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
rcases Set.eq_empty_or_nonempty s with (rfl | ⟨⟨p₁, hp₁⟩⟩)

Premises used: Set.eq_empty_or_nonempty, 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
⊢ Collinear.{u_1, u_2, u_3} k (P := P) ∅ ↔
    ∃ (p₀ : P) (v : V), ∀ (p : P), Membership.mem (γ := Set P) ∅ p → ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
simp [collinear_empty]

Premises used: collinear_empty
-- 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
inr : (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
⊢ Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
rw [collinear_iff_of_mem hp₁]

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
hp₁ : p₁ ∈ s
inr : (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) → ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
inr₁ : (∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀) → ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
⊢ (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
constructor
-- 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), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) → ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
fun h => ⟨p₁, h⟩

Premises used: 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), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) → ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
exact fun h => ⟨p₁, 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
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
⊢ ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁

Tactic:
use v
-- 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
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
h : ∀ (r : k) (hp₂ : r • v +ᵥ p ∈ s), ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ p₁
⊢ ∃ (r : k), p₂ = r • v +ᵥ p₁

Tactic:
rcases hv 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
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
h : ∀ (r₁ : k) (hp₁ : r₁ • v +ᵥ p ∈ s), ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ r₁ • v +ᵥ p
⊢ ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ p₁

Tactic:
rcases hv 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
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
h : r • v +ᵥ p = (r - r₁) • v +ᵥ r₁ • v +ᵥ p
⊢ ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ r₁ • v +ᵥ p

Tactic:
use 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
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
⊢ r • v +ᵥ p = (r - r₁) • v +ᵥ r₁ • v +ᵥ p

Tactic:
simp [vadd_vadd, ← add_smul]

Premises used: vadd_vadd, add_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
p₁ p₂ : P
rw : ∃ (p₀ : P) (v : V), ∀ (p : P), Membership.mem (γ := Set P) {p₁, p₂} p → ∃ (r : k), p = r • v +ᵥ p₀
⊢ Collinear k (P := P) {p₁, p₂}

Tactic:
rw [collinear_iff_exists_forall_eq_smul_vadd]

Premises used: collinear_iff_exists_forall_eq_smul_vadd
-- 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 : ∀ (p : P), Membership.mem (γ := Set P) {p₁, p₂} p → ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ ∃ (p₀ : P) (v : V), ∀ (p : P), Membership.mem (γ := Set P) {p₁, p₂} p → ∃ (r : k), p = r • v +ᵥ p₀

Tactic:
use p₁, p₂ -ᵥ 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
p₁ p₂ p : P
hp : Membership.mem (γ := Set P) {p₁, p₂} p
⊢ p = p₁ ∨ p = p₂

Tactic:
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp

Premises used: Set.mem_singleton_iff, Set.mem_insert_iff
-- 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
hp : p = p₁ ∨ p = p₂
h : ∀ (hp : p = p₁), ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
h₁ : ∀ (hp : p = p₂), ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
rcases hp with hp | hp
-- 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
hp : p = p₁
h : p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (p₂ -ᵥ p₁) +ᵥ p₁
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
use 0
-- 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
hp : p = p₁
⊢ p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
simp [hp]
-- 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
hp : p = p₂
h : p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₂ -ᵥ p₁) +ᵥ p₁
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
use 1
-- 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
hp : p = p₂
⊢ p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
simp [hp]
-- 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
rw : AffineIndependent k p ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1
rw₁ rw₂ :
  ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1 ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1
⊢ AffineIndependent k p ↔ ¬Collinear k (Set.range p)

Tactic:
rw [collinear_iff_finrank_le_one,
    affineIndependent_iff_not_finrank_vectorSpan_le k p (Fintype.card_fin 3)]

Premises used: Fintype.card_fin, collinear_iff_finrank_le_one, affineIndependent_iff_not_finrank_vectorSpan_le, OfNat.ofNat
-- 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
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1 ↔ ¬AffineIndependent k p
rw₁ rw₂ : ¬AffineIndependent k p ↔ ¬AffineIndependent k p
⊢ Collinear k (Set.range p) ↔ ¬AffineIndependent k p

Tactic:
rw [collinear_iff_finrank_le_one,
    finrank_vectorSpan_le_iff_not_affineIndependent k p (Fintype.card_fin 3)]

Premises used: Fintype.card_fin, finrank_vectorSpan_le_iff_not_affineIndependent, collinear_iff_finrank_le_one, OfNat.ofNat
-- 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
rw : ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
⊢ AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
rw [affineIndependent_iff_not_collinear]

Premises used: affineIndependent_iff_not_collinear