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 : 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)))
h' : s.direction ≤ vectorSpan k (insert p (↑s : Set P))
⊢ False

Tactic:
hf (Submodule.finiteDimensional_of_le h')

Premises used: Submodule.finiteDimensional_of_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 : 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)))
h' : s.direction ≤ vectorSpan k (insert p (↑s : Set P))
⊢ False

Tactic:
exact hf (Submodule.finiteDimensional_of_le h')

Premises used: Submodule.finiteDimensional_of_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 : AffineSubspace k P
p : P
hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction
⊢ ¬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')
-- 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 : 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)))
neg : LE.le (α := ℕ) 0 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1

Tactic:
rw [finrank_of_infinite_dimensional hf, finrank_of_infinite_dimensional hf', zero_add]

Premises used: zero_add, Module.finrank_of_infinite_dimensional
-- 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 : 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)))
⊢ LE.le (α := ℕ) 0 1

Tactic:
zero_le_one

Premises used: zero_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 : 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)))
⊢ LE.le (α := ℕ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
pos :
  finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : 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

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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
pos :
  ∀ (hs : (↑s : Set P) = ∅),
    finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
      finrank.{u_1, u_2} k ↥s.direction + 1
pos₁ :
  ∀ (p₀ : P) (hp₀ : p₀ ∈ (↑s : Set P)),
    finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
      finrank.{u_1, u_2} k ↥s.direction + 1
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1

Tactic:
rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)

Premises used: Set.eq_empty_or_nonempty, SetLike.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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : (↑s : Set P) = ∅
⊢ s = ⊥

Tactic:
rw [coe_eq_bot_iff] at hs

Premises used: AffineSubspace.coe_eq_bot_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
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
pos : finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) ≤ 1
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1

Tactic:
rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan, direction_bot, finrank_bot,
      zero_add]

Premises used: direction_affineSpan, AffineSubspace.bot_coe, zero_add, AffineSubspace.span_empty, AffineSubspace.direction_bot, finrank_bot
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
⊢ LE.le (α := ℕ) 0 1

Tactic:
zero_le_one' ℕ

Premises used: zero_le_one', Nat
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
h : finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = 0
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) ≤ 1

Tactic:
convert! zero_le_one' ℕ

Premises used: zero_le_one', Nat
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
h : finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = finrank.{u_1, u_2} k ↥⊥
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = 0

Tactic:
rw [← finrank_bot k V]

Premises used: finrank_bot
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) =
    finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅))

Tactic:
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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
h : ∀ (x : V), Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
h₁ :
  ↥⊥ = ↥(vectorSpan k (P := P) (insert p ∅)) →
    Eq.{u_1 + 1} (α := Semiring k) DivisionSemiring.toSemiring Ring.toSemiring →
      inst_2 ≍ inst_2 → Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
h₂ :
  ↥⊥ = ↥(vectorSpan k (P := P) (insert p ∅)) →
    HEq (α := AddCommMonoid ↥⊥) (Submodule.addCommMonoid ⊥) (β := AddCommMonoid ↥(vectorSpan k (P := P) (insert p ∅)))
        (Submodule.addCommMonoid (vectorSpan k (P := P) (insert p ∅))) →
      Eq.{u_1 + 1} (α := Semiring k) DivisionSemiring.toSemiring Ring.toSemiring →
        inst_2 ≍ inst_2 → Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = finrank.{u_1, u_2} k ↥⊥

Tactic:
convert! 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
x : V
⊢ Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
e_2 : ↥⊥ = ↥(vectorSpan k (P := P) (insert p ∅))
e_3 : Eq.{u_1 + 1} (α := Semiring k) DivisionSemiring.toSemiring Ring.toSemiring
e_5 : inst_2 ≍ inst_2
⊢ Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
e_2 : ↥⊥ = ↥(vectorSpan k (P := P) (insert p ∅))
e_4 :
  HEq (α := AddCommMonoid ↥⊥) (Submodule.addCommMonoid ⊥) (β := AddCommMonoid ↥(vectorSpan k (P := P) (insert p ∅)))
    (Submodule.addCommMonoid (vectorSpan k (P := P) (insert p ∅)))
e_3 : Eq.{u_1 + 1} (α := Semiring k) DivisionSemiring.toSemiring Ring.toSemiring
e_5 : inst_2 ≍ inst_2
⊢ Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
pos : finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction) ≤ 1 + finrank.{u_1, u_2} k ↥s.direction
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1

Tactic:
rw [affineSpan_coe, direction_affineSpan_insert hp₀, add_comm]

Premises used: AffineSubspace.direction_affineSpan_insert, add_comm, AffineSubspace.affineSpan_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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction) ≤ 1 + finrank.{u_1, u_2} k ↥s.direction

Tactic:
(Submodule.finrank_add_le_finrank_add_finrank _ _).trans ?_

Premises used: Set.Mem, setOf, Submodule.finrank_add_le_finrank_add_finrank, 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
pos : finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) + finrank.{u_1, u_2} k ↥s.direction ≤ 1 + finrank.{u_1, u_2} k ↥s.direction
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction) ≤ 1 + finrank.{u_1, u_2} k ↥s.direction

Tactic:
refine (Submodule.finrank_add_le_finrank_add_finrank _ _).trans ?_

Premises used: Submodule.finrank_add_le_finrank_add_finrank, 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
pos : finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) ≤ 1
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) + finrank.{u_1, u_2} k ↥s.direction ≤ 1 + finrank.{u_1, u_2} k ↥s.direction

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
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) ≤ 1

Tactic:
finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => ?_

Premises used: Submodule.mem_span_singleton_self, VSub.vsub, Subtype.mk, finrank_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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
pos :
  ∀ (v : ↥(k ∙ (p -ᵥ p₀))),
    ∃ (c : k),
      HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
          (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
        v
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) ≤ 1

Tactic:
refine finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => ?_

Premises used: finrank_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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
⊢ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) (↑v : V)

Tactic:
have h := v.property
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
h : Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) (↑v : V)
⊢ ∃ (a : k), a • (p -ᵥ p₀) = (↑v : V)

Tactic:
rw [Submodule.mem_span_singleton] at h

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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
h : ∃ (a : k), a • (p -ᵥ p₀) = (↑v : V)
pos :
  ∀ (c : k) (hc : c • (p -ᵥ p₀) = (↑v : V)),
    ∃ (c : k),
      HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
          (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
        v
⊢ ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
      v

Tactic:
rcases h with ⟨c, hc⟩
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = (↑v : V)
⊢ ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
      v

Tactic:
⟨c, ?_⟩

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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = (↑v : V)
pos :
  HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
    v
⊢ ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
      v

Tactic:
refine ⟨c, ?_⟩
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = (↑v : V)
pos :
  (↑(HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
          (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯)) :
      V) =
    (↑v : V)
⊢ HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
    v

Tactic:
ext
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = (↑v : V)
⊢ (↑(HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
          (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯)) :
      V) =
    (↑v : V)

Tactic:
hc
-- 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 : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = (↑v : V)
⊢ (↑(HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
          (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯)) :
      V) =
    (↑v : V)

Tactic:
exact hc
-- 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
rw :
  finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P))) ≤
    finrank.{u_1, u_2} k ↥(direction (affineSpan k s)) + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p s)) ≤ finrank.{u_1, u_2} k ↥(vectorSpan k s) + 1

Tactic:
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan,
    ← direction_affineSpan _ s]

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
p : P
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P))) ≤
    finrank.{u_1, u_2} k ↥(direction (affineSpan k s)) + 1

Tactic:
finrank_vectorSpan_insert_le ..

Premises used: finrank_vectorSpan_insert_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
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P))) ≤
    finrank.{u_1, u_2} k ↥(direction (affineSpan k s)) + 1

Tactic:
exact finrank_vectorSpan_insert_le ..

Premises used: finrank_vectorSpan_insert_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
h : Collinear k s
p : P
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)

Tactic:
have : FiniteDimensional k { x // x ∈ vectorSpan k s } := h.finiteDimensional_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
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
grw : finrank.{u_1, u_2} k ↥(vectorSpan k (insert p s)) ≤ 2
grw₁ : finrank.{u_1, u_2} k ↥(vectorSpan k s) + 1 ≤ 2
grw₂ grw₃ : HAdd.hAdd (α := ℕ) 1 1 ≤ HAdd.hAdd (α := ℕ) 1 1
⊢ Coplanar k (insert p s)

Tactic:
grw [coplanar_iff_finrank_le_two, finrank_vectorSpan_insert_le_set, h.finrank_le_one]

Premises used: Collinear.finrank_le_one, coplanar_iff_finrank_le_two, finrank_vectorSpan_insert_le_set
-- 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 : finrank k V = 2
⊢ FiniteDimensional k V

Tactic:
have : FiniteDimensional k V := .of_finrank_eq_succ 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
h : finrank k V = 2
this : FiniteDimensional k V
rw : finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ finrank k V
⊢ Coplanar k s

Tactic:
rw [coplanar_iff_finrank_le_two, ← h]

Premises used: coplanar_iff_finrank_le_two
-- 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 : finrank k V = 2
this : FiniteDimensional k V
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ finrank k V

Tactic:
Submodule.finrank_le _

Premises used: Submodule.finrank_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
h : finrank k V = 2
this : FiniteDimensional k V
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ finrank k V

Tactic:
exact Submodule.finrank_le _

Premises used: Submodule.finrank_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
h : Fact (finrank k V = 2)
⊢ Coplanar k s

Tactic:
coplanar_of_finrank_eq_two s h.out

Premises used: coplanar_of_finrank_eq_two, Fact.out
-- 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
⊢ Coplanar k (P := P) {p₁, p₂, p₃}

Tactic:
(collinear_pair k p₂ p₃).coplanar_insert p₁

Premises used: Collinear.coplanar_insert, 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
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i}) (s.points i)
⊢ Collinear k (P := P) {s.points i, s.centroid, s.faceOppositeCentroid i}

Tactic:
apply collinear_insert_of_mem_affineSpan_pair

Premises used: collinear_insert_of_mem_affineSpan_pair