awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range p)) ⊤
have hc₁ : 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
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ Eq (α := AffineSubspace k V) (affineSpan k (Set.range T.points)) ⊤
have rw : Fintype.card (Fin (n + 1)) = finrank k V + 1
Tactic: rw [AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one T.independent,
    Fintype.card_fin, hrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ Eq (α := AffineSubspace k V) (affineSpan k (Set.range T.points)) ⊤
have rw₁ : n + 1 = finrank k V + 1
Tactic: rw [AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one T.independent,
    Fintype.card_fin, hrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ Eq (α := AffineSubspace k V) (affineSpan k (Set.range T.points)) ⊤
have rw₂ : n + 1 = n + 1
Tactic: rw [AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one T.independent,
    Fintype.card_fin, hrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 ↥(vectorSpan k (insert p (↑s : Set P)))
have rw : FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : 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 (↑(affineSpan k (↑s : Set P)) : Set P))))
have inl : ∀ (hs : (↑s : 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₀⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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))))
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
have 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))))
Tactic: rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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) = ∅
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
have hs₁ : s = ⊥
Tactic: rw [coe_eq_bot_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
have inl : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅))
Tactic: rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 ↥(vectorSpan k (P := P) (insert p ∅))
have h : ∀ (x : V), Eq (α := Submodule k V) (vectorSpan k (P := P) (insert p ∅)) ⊥
Tactic: convert! finiteDimensional_bot k V
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 ∅)) ⊥
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅))
have h₁ : ↥(vectorSpan k (P := P) (insert p ∅)) = ↥⊥ → Eq (α := Submodule k V) (vectorSpan k (P := P) (insert p ∅)) ⊥
Tactic: convert! finiteDimensional_bot k V
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 ∅)) ⊥
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅))
have 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 ∅)) ⊥
Tactic: convert! finiteDimensional_bot k V
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P))))
have inr : FiniteDimensional.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction)
Tactic: rw [affineSpan_coe, direction_affineSpan_insert hp₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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 ↥(vectorSpan k (insert p s))
have this : FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))
Tactic: haveI : FiniteDimensional k (affineSpan k s).direction :=
    (direction_affineSpan k s).symm ▸ inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 s))
have rw : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P)))
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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 ↥(direction (affineSpan k (insert p s)))
have this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
Tactic: haveI : FiniteDimensional k (vectorSpan k s) := (direction_affineSpan k s) ▸ inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 ↥(direction (affineSpan k (insert p s)))
have rw : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p s))
Tactic: rw [direction_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
⊢ Collinear k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 1
have h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
Tactic: have h := collinear_iff_rank_le_one k s
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 1
have 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
Tactic: rw [← finrank_eq_rank] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
⊢ Collinear.{u_1, u_2, u_3} k (P := P) ∅
have rw : Module.rank k ↥⊥ ≤ 1
Tactic: rw [collinear_iff_rank_le_one, vectorSpan_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : P
⊢ Collinear k (P := P) {p}
have rw : Module.rank k ↥⊥ ≤ 1
Tactic: rw [collinear_iff_rank_le_one, vectorSpan_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ Collinear k s ↔ ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
have 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₀
Tactic: simp_rw [collinear_iff_rank_le_one, rank_submodule_le_one_iff', Submodule.le_span_singleton_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ (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₀
have 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₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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₀
⊢ (∃ (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₀
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (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₀
have h₁ : ∀ p ∈ s, ∃ (r : k), p = r • v₀ +ᵥ p₀
Tactic: use v₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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), p = r • v₀ +ᵥ p₀
have h₁ : ∀ (r : k) (hr : r • v₀ = p -ᵥ p₀), ∃ (r : k), p = r • v₀ +ᵥ p₀
Tactic: obtain ⟨r, hr⟩ := hv (p -ᵥ p₀) (vsub_mem_vectorSpan k hp h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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₀
⊢ ∃ (r : k), p = r • v₀ +ᵥ p₀
have h₁ : p = r • v₀ +ᵥ p₀
Tactic: use r
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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 = r • v₀ +ᵥ p₀
have h₁ : p -ᵥ p₀ = r • v₀
Tactic: rw [eq_vadd_iff_vsub_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀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
have h₁ : ∀ (v_1 : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v_1 → ∃ (r : k), r • v = v_1
Tactic: use v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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)
have rw : ∀ (x : V), Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p₀) '' s) x → x ∈ (↑(k ∙ v) : Set V)
Tactic: rw [vectorSpan_eq_span_vsub_set_right k h, Submodule.span_le, Set.subset_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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 ∈ (↑(k ∙ v) : Set V)
have rw : ∃ (a : k), a • v = x
Tactic: rw [SetLike.mem_coe, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
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
⊢ ∃ (a : k), a • v = x
have hx₁ : ∃ x_1 ∈ s, x_1 -ᵥ p₀ = x
Tactic: rw [Set.mem_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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
⊢ ∃ (a : k), a • v = x
have rcases : ∀ (p : P) (hp : p ∈ s), ∃ (a : k), a • v = p -ᵥ p₀
Tactic: rcases hx with ⟨p, hp, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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
⊢ ∃ (a : k), a • v = p -ᵥ p₀
have rcases : ∀ (r : k) (hp : r • v +ᵥ p₀ ∈ s), ∃ (a : k), a • v = (r • v +ᵥ p₀) -ᵥ p₀
Tactic: rcases hp₀v p hp with ⟨r, rfl⟩
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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
⊢ ∃ (a : k), a • v = (r • v +ᵥ p₀) -ᵥ p₀
have h₁ : r • v = (r • v +ᵥ p₀) -ᵥ p₀
Tactic: use r
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
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), r • v = w
have hs : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
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)
⊢ ∃ (r : k), r • v = w
have hw' : Membership.mem (γ := Submodule k V) (k ∙ v) w
Tactic: have hw' := SetLike.le_def.1 hs hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₀ : P
h : 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
⊢ ∃ (r : k), r • v = w
have h₁ : ∀ (hw' : ∃ (a : k), a • v = w), ∃ (r : k), r • v = w
Tactic: rwa [Submodule.mem_span_singleton] at hw'
Cleared hypotheses: hw'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
⊢ Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
have 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₀
Tactic: rcases Set.eq_empty_or_nonempty s with (rfl | ⟨⟨p₁, hp₁⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
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₀
⊢ Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
have inr : ∀ (p₁ : P) (hp₁ : p₁ ∈ s), 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₁⟩⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
have inr : (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
Tactic: rw [collinear_iff_of_mem hp₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₁ : P
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₀
have inr : (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) → ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
Tactic: constructor