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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
hn : s.Nonempty
refine : direction (affineSpan k (↑(Finset.image p s) : Set P)) = sp.direction
⊢ affineSpan k (↑(Finset.image p s) : Set P) = sp

Tactic:
refine eq_of_direction_eq_of_nonempty_of_le ?_ ((hn.image p).to_set.affineSpan k) hle

Premises used: Finset.Nonempty.image, AffineSubspace.eq_of_direction_eq_of_nonempty_of_le, Set.Nonempty.affineSpan, Finset.Nonempty.to_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
hn : s.Nonempty
⊢ direction (affineSpan k (↑(Finset.image p s) : Set P)) ≤ sp.direction

Tactic:
have hd := direction_le hle
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
hn : s.Nonempty
hd : direction (affineSpan k (↑(Finset.image p s) : Set P)) ≤ sp.direction
rw :
  ∀ (hd : vectorSpan k (↑(Finset.image p s) : Set P) ≤ sp.direction),
    vectorSpan k (↑(Finset.image p s) : Set P) = sp.direction
⊢ direction (affineSpan k (↑(Finset.image p s) : Set P)) = sp.direction

Tactic:
rw [direction_affineSpan] at hd ⊢

Premises used: direction_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
hn : s.Nonempty
hd : vectorSpan k (↑(Finset.image p s) : Set P) ≤ sp.direction
⊢ vectorSpan k (↑(Finset.image p s) : Set P) = sp.direction

Tactic:
hi.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc

Premises used: AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p s) : Set P) ≤ sp
hc : #s = finrank.{u_1, u_2} k ↥sp.direction + 1
hn : s.Nonempty
hd : vectorSpan k (↑(Finset.image p s) : Set P) ≤ sp.direction
⊢ vectorSpan k (↑(Finset.image p s) : Set P) = sp.direction

Tactic:
exact hi.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc

Premises used: AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1

Tactic:
rw [← Finset.card_univ] at hc

Premises used: Finset.card_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1
rw :
  ∀ (hle : affineSpan k (↑(Finset.image p Finset.univ) : Set P) ≤ sp)
    (hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1),
    affineSpan k (↑(Finset.image p Finset.univ) : Set P) = sp
⊢ affineSpan k (Set.range p) = sp

Tactic:
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p Finset.univ) : Set P) ≤ sp
hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ affineSpan k (↑(Finset.image p Finset.univ) : Set P) = sp

Tactic:
hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc

Premises used: AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (↑(Finset.image p Finset.univ) : Set P) ≤ sp
hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1
⊢ affineSpan k (↑(Finset.image p Finset.univ) : Set P) = sp

Tactic:
exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc

Premises used: AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst_5 : FiniteDimensional.{u_1, u_2} k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥sp.direction + 1
rw rw₁ rw₂ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1),
    affineSpan k (Set.range p) = sp
rw₃ :
  ∀ (hle : affineSpan k (↑(Finset.image p Finset.univ) : Set P) ≤ sp)
    (hc : Finset.card.{u_4} (α := ι) Finset.univ = finrank.{u_1, u_2} k ↥sp.direction + 1),
    affineSpan k (↑(Finset.image p Finset.univ) : Set P) = sp
⊢ affineSpan k (Set.range p) = sp

Tactic:
classical
  rw [← Finset.card_univ] at hc
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢
  exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc

Premises used: Finset.card_univ, Set.image_univ, Finset.coe_univ, Finset.coe_image
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
mp : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤ → Fintype.card ι = finrank k V + 1
mpr : Fintype.card ι = finrank k V + 1 → Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤ ↔ Fintype.card ι = finrank k V + 1

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
n : ℕ := Fintype.card ι - 1
⊢ Fintype.card ι = n + 1

Tactic:
have hn : Fintype.card ι = n + 1 :=
      (Nat.succ_pred_eq_of_pos (card_pos_of_affineSpan_eq_top k V P h_tot)).symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
mp : n + 1 = finrank k V + 1
mp₁ : n + 1 = finrank.{u_1, u_2} k ↥⊤ + 1
mp₂ : n + 1 = finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
mp₃ mp₄ :
  finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1 = finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
⊢ Fintype.card ι = finrank k V + 1

Tactic:
rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
      ← hi.finrank_vectorSpan hn]

Premises used: finrank_top, AffineIndependent.finrank_vectorSpan, AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k V + 1
⊢ Fintype.card ι = finrank.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊤) + 1

Tactic:
rw [← finrank_top, ← direction_top k V P] at hc

Premises used: AffineSubspace.direction_top, finrank_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊤) + 1
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤

Tactic:
hi.affineSpan_eq_of_le_of_card_eq_finrank_add_one le_top hc

Premises used: AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one, le_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
inst_5 : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊤) + 1
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤

Tactic:
exact hi.affineSpan_eq_of_le_of_card_eq_finrank_add_one le_top hc

Premises used: AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one, le_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : FiniteDimensional k V
n : ℕ
T : Simplex k V n
hrank : finrank k V = n
rw : Fintype.card (Fin (n + 1)) = finrank k V + 1
rw₁ : n + 1 = finrank k V + 1
rw₂ rw₃ : n + 1 = n + 1
⊢ Eq (α := AffineSubspace k V) (affineSpan k (Set.range T.points)) ⊤

Tactic:
rw [AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one T.independent,
    Fintype.card_fin, hrank]

Premises used: Fintype.card_fin, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one, Affine.Simplex.independent
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
rw : FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set 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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
inl :
  ∀ (hs : (↑s : Set P) = ∅),
    FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
inr :
  ∀ (p₀ : P) (hp₀ : p₀ ∈ (↑s : Set P)),
    FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))

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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
hs : s = ⊥
inl : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅))
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))

Tactic:
rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan]

Premises used: direction_affineSpan, AffineSubspace.bot_coe, AffineSubspace.span_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
hs : s = ⊥
⊢ FiniteDimensional.{u_1, u_2} k ↥⊥

Tactic:
finiteDimensional_bot k V

Premises used: finiteDimensional_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
hs : s = ⊥
h : ∀ (x : V), Eq (α := Submodule k V) (vectorSpan k (P := P) (insert p ∅)) ⊥
h₁ : ↥(vectorSpan k (P := P) (insert p ∅)) = ↥⊥ → Eq (α := Submodule k V) (vectorSpan k (P := P) (insert p ∅)) ⊥
h₂ :
  ↥(vectorSpan k (P := P) (insert p ∅)) = ↥⊥ →
    HEq (α := AddCommGroup ↥(vectorSpan k (P := P) (insert p ∅)))
        (Submodule.addCommGroup (vectorSpan k (P := P) (insert p ∅))) (β := AddCommGroup ↥⊥)
        (Submodule.addCommGroup ⊥) →
      Eq.{u_1 + 1} (α := Semiring k) Ring.toSemiring DivisionSemiring.toSemiring →
        inst_2 ≍ inst_2 → Eq (α := Submodule k V) (vectorSpan k (P := P) (insert p ∅)) ⊥
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅))

Tactic:
convert! finiteDimensional_bot k V

Premises used: finiteDimensional_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
hs : s = ⊥
e_2 : ↥(vectorSpan k (P := P) (insert p ∅)) = ↥⊥
⊢ 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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
hs : s = ⊥
e_2 : ↥(vectorSpan k (P := P) (insert p ∅)) = ↥⊥
e_4 :
  HEq (α := AddCommGroup ↥(vectorSpan k (P := P) (insert p ∅)))
    (Submodule.addCommGroup (vectorSpan k (P := P) (insert p ∅))) (β := AddCommGroup ↥⊥) (Submodule.addCommGroup ⊥)
e_3 : Eq.{u_1 + 1} (α := Semiring k) Ring.toSemiring DivisionSemiring.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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
inr : FiniteDimensional.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction)
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))

Tactic:
rw [affineSpan_coe, direction_affineSpan_insert hp₀]

Premises used: AffineSubspace.direction_affineSpan_insert, AffineSubspace.affineSpan_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
⊢ FiniteDimensional.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s.direction
p : P
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑s : Set P))))

Tactic:
(direction_affineSpan k (insert p (s : Set P))).symm ▸ finiteDimensional_vectorSpan_insert s p

Premises used: direction_affineSpan, Eq.rec, Insert.insert, SetLike.coe, Eq.symm, finiteDimensional_vectorSpan_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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)
p : P
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))

Tactic:
haveI : FiniteDimensional k (affineSpan k s).direction :=
    (direction_affineSpan k s).symm ▸ inferInstance
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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)
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))
rw : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P)))
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p s))

Tactic:
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_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
ι : Type u_4
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)
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P)))

Tactic:
finiteDimensional_vectorSpan_insert (affineSpan k s) p

Premises used: affineSpan, finiteDimensional_vectorSpan_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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)
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P)))

Tactic:
exact finiteDimensional_vectorSpan_insert (affineSpan k s) p

Premises used: affineSpan, finiteDimensional_vectorSpan_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(direction (affineSpan k s))
p : P
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)

Tactic:
haveI : FiniteDimensional k (vectorSpan k s) := (direction_affineSpan k s) ▸ inferInstance
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(direction (affineSpan k s))
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
rw : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p s))
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p s)))

Tactic:
rw [direction_affineSpan]

Premises used: direction_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(direction (affineSpan k s))
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p s))

Tactic:
infer_instance
-- 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
⊢ Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1

Tactic:
Iff.rfl

Premises used: Collinear, Iff.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
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
⊢ Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1

Tactic:
have h := collinear_iff_rank_le_one k s