[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
⊢ _root_.Finite ι
[PROOFSTEP]
nontriviality ι
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
✝ : Nontrivial ι
⊢ _root_.Finite ι
[PROOFSTEP]
inhabit ι
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
✝ : Nontrivial ι
inhabited_h : Inhabited ι
⊢ _root_.Finite ι
[PROOFSTEP]
rw [affineIndependent_iff_linearIndependent_vsub k p default] at hi 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
✝ : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent k fun i => p ↑i -ᵥ p default
⊢ _root_.Finite ι
[PROOFSTEP]
letI : IsNoetherian k V := IsNoetherian.iff_fg.2 inferInstance
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
✝ : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent k fun i => p ↑i -ᵥ p default
this : IsNoetherian k V := Iff.mpr IsNoetherian.iff_fg inferInstance
⊢ _root_.Finite ι
[PROOFSTEP]
exact (Set.finite_singleton default).finite_of_compl (Set.finite_coe_iff.1 hi.finite_of_isNoetherian)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
classical
have hi' := hi.range.mono (Set.image_subset_range p ↑s)
have hc' : (s.image p).card = n + 1 := by rwa [s.card_image_of_injective hi.injective]
have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
rcases hn with ⟨p₁, hp₁⟩
have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton, ← Finset.coe_image, ←
  Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image] at hi' 
have hc : (Finset.image (fun p : P => p -ᵥ p₁) ((Finset.image p s).erase p₁)).card = n :=
  by
  rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
  exact Nat.pred_eq_of_eq_succ hc'
rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
have hi' := hi.range.mono (Set.image_subset_range p ↑s)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
have hc' : (s.image p).card = n + 1 := by rwa [s.card_image_of_injective hi.injective]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
⊢ Finset.card (Finset.image p s) = n + 1
[PROOFSTEP]
rwa [s.card_image_of_injective hi.injective]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
hc' : Finset.card (Finset.image p s) = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
hc' : Finset.card (Finset.image p s) = n + 1
⊢ Finset.Nonempty (Finset.image p s)
[PROOFSTEP]
simp [hc', ← Finset.card_pos]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
hc' : Finset.card (Finset.image p s) = n + 1
hn : Finset.Nonempty (Finset.image p s)
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
rcases hn with ⟨p₁, hp₁⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
hc' : Finset.card (Finset.image p s) = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
hc' : Finset.card (Finset.image p s) = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ p₁ ∈ p '' ↑s
[PROOFSTEP]
simpa using hp₁
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hi' : AffineIndependent k fun x => ↑x
hc' : Finset.card (Finset.image p s) = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton, ← Finset.coe_image, ←
  Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image] at hi' 
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hc' : Finset.card (Finset.image p s) = n + 1
p₁ : P
hi'✝² : LinearIndependent k fun v => ↑v
hi'✝¹ : LinearIndependent k fun v => ↑v
hi'✝ : LinearIndependent k fun v => ↑v
hi' : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
have hc : (Finset.image (fun p : P => p -ᵥ p₁) ((Finset.image p s).erase p₁)).card = n :=
  by
  rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
  exact Nat.pred_eq_of_eq_succ hc'
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hc' : Finset.card (Finset.image p s) = n + 1
p₁ : P
hi'✝² : LinearIndependent k fun v => ↑v
hi'✝¹ : LinearIndependent k fun v => ↑v
hi'✝ : LinearIndependent k fun v => ↑v
hi' : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ Finset.card (Finset.image (fun p => p -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) = n
[PROOFSTEP]
rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hc' : Finset.card (Finset.image p s) = n + 1
p₁ : P
hi'✝² : LinearIndependent k fun v => ↑v
hi'✝¹ : LinearIndependent k fun v => ↑v
hi'✝ : LinearIndependent k fun v => ↑v
hi' : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ Finset.card (Finset.image p s) - 1 = n
[PROOFSTEP]
exact Nat.pred_eq_of_eq_succ hc'
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc✝ : Finset.card s = n + 1
hc' : Finset.card (Finset.image p s) = n + 1
p₁ : P
hi'✝² : LinearIndependent k fun v => ↑v
hi'✝¹ : LinearIndependent k fun v => ↑v
hi'✝ : LinearIndependent k fun v => ↑v
hi' : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
hc : Finset.card (Finset.image (fun p => p -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) = n
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n
[PROOFSTEP]
rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
classical
rw [← Finset.card_univ] at hc 
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
exact hi.finrank_vectorSpan_image_finset hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
rw [← Finset.card_univ] at hc 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : Finset.card Finset.univ = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : Finset.card Finset.univ = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p Finset.univ) } = n
[PROOFSTEP]
exact hi.finrank_vectorSpan_image_finset hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
[PROOFSTEP]
classical
have hn : (s.image p).Nonempty :=
  by
  rw [Finset.Nonempty.image_iff, ← Finset.card_pos, hc]
  apply Nat.succ_pos
rcases hn with ⟨p₁, hp₁⟩
rw [vectorSpan_eq_span_vsub_finset_right_ne k hp₁]
refine' le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) _
rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁, tsub_le_iff_right, ← hc]
apply Finset.card_image_le
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
[PROOFSTEP]
have hn : (s.image p).Nonempty :=
  by
  rw [Finset.Nonempty.image_iff, ← Finset.card_pos, hc]
  apply Nat.succ_pos
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ Finset.Nonempty (Finset.image p s)
[PROOFSTEP]
rw [Finset.Nonempty.image_iff, ← Finset.card_pos, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
⊢ 0 < n + 1
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
hn : Finset.Nonempty (Finset.image p s)
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
[PROOFSTEP]
rcases hn with ⟨p₁, hp₁⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_finset_right_ne k hp₁]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k { x // x ∈ Submodule.span k ↑(Finset.image (fun x => x -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) } ≤ n
[PROOFSTEP]
refine' le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) _
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ Finset.card (Finset.image (fun p => p -ᵥ p₁) (Finset.erase (Finset.image p s) p₁)) ≤ n
[PROOFSTEP]
rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁, tsub_le_iff_right, ← hc]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : Finset.card s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ Finset.card (Finset.image p s) ≤ Finset.card s
[PROOFSTEP]
apply Finset.card_image_le
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ n
[PROOFSTEP]
classical
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
rw [← Finset.card_univ] at hc 
exact finrank_vectorSpan_image_finset_le _ _ _ hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ n
[PROOFSTEP]
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p Finset.univ) } ≤ n
[PROOFSTEP]
rw [← Finset.card_univ] at hc 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card Finset.univ = n + 1
⊢ finrank k { x // x ∈ vectorSpan k ↑(Finset.image p Finset.univ) } ≤ n
[PROOFSTEP]
exact finrank_vectorSpan_image_finset_le _ _ _ hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
classical
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
cases' hn with i₁
rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁, linearIndependent_iff_card_eq_finrank_span, eq_comm,
  vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
congr
rw [← Finset.card_univ] at hc 
rw [Fintype.subtype_card]
simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ Nonempty ι
[PROOFSTEP]
simp [← Fintype.card_pos_iff, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
hn : Nonempty ι
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
cases' hn with i₁
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁, linearIndependent_iff_card_eq_finrank_span, eq_comm,
  vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
[PROOFSTEP]
congr
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
[PROOFSTEP]
rw [← Finset.card_univ] at hc 
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card Finset.univ = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
[PROOFSTEP]
rw [Fintype.subtype_card]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card Finset.univ = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } =
      Finset.card (Finset.filter (fun x => x ≠ i₁) Finset.univ) ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
[PROOFSTEP]
simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
[PROOFSTEP]
rw [affineIndependent_iff_finrank_vectorSpan_eq k p hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n ↔ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n → n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hc : Fintype.card ι = finrank k { x // x ∈ vectorSpan k (Set.range p) } + 1
⊢ finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) }
[PROOFSTEP]
rfl
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ n ≤ finrank k { x // x ∈ vectorSpan k (Set.range p) } → finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
[PROOFSTEP]
exact fun hle => le_antisymm (finrank_vectorSpan_range_le k p hc) hle
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
⊢ AffineIndependent k p ↔ ¬finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ n
[PROOFSTEP]
rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k ↑(Finset.image p s) = sp
[PROOFSTEP]
have hn : s.Nonempty := by
  rw [← Finset.card_pos, hc]
  apply Nat.succ_pos
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
⊢ Finset.Nonempty s
[PROOFSTEP]
rw [← Finset.card_pos, hc]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
⊢ 0 < finrank k { x // x ∈ direction sp } + 1
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
⊢ affineSpan k ↑(Finset.image p s) = sp
[PROOFSTEP]
refine' eq_of_direction_eq_of_nonempty_of_le _ ((hn.image p).to_set.affineSpan k) hle
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
⊢ direction (affineSpan k ↑(Finset.image p s)) = direction sp
[PROOFSTEP]
have hd := direction_le hle
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
hd : direction (affineSpan k ↑(Finset.image p s)) ≤ direction sp
⊢ direction (affineSpan k ↑(Finset.image p s)) = direction sp
[PROOFSTEP]
rw [direction_affineSpan] at hd ⊢
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : Finset.card s = finrank k { x // x ∈ direction sp } + 1
hn : Finset.Nonempty s
hd : vectorSpan k ↑(Finset.image p s) ≤ direction sp
⊢ vectorSpan k ↑(Finset.image p s) = direction sp
[PROOFSTEP]
exact hi.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k (Set.range p) = sp
[PROOFSTEP]
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
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k (Set.range p) = sp
[PROOFSTEP]
rw [← Finset.card_univ] at hc 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k (Set.range p) ≤ sp
hc : Finset.card Finset.univ = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k (Set.range p) = sp
[PROOFSTEP]
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle✝¹ : affineSpan k (p '' Set.univ) ≤ sp
hle✝ : affineSpan k (p '' ↑Finset.univ) ≤ sp
hle : affineSpan k ↑(Finset.image p Finset.univ) ≤ sp
hc : Finset.card Finset.univ = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k ↑(Finset.image p Finset.univ) = sp
[PROOFSTEP]
exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = finrank k V + 1
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ affineSpan k (Set.range p) = ⊤ → Fintype.card ι = finrank k V + 1
[PROOFSTEP]
intro h_tot
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
⊢ Fintype.card ι = finrank k V + 1
[PROOFSTEP]
let n := Fintype.card ι - 1
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
⊢ Fintype.card ι = finrank k V + 1
[PROOFSTEP]
have hn : Fintype.card ι = n + 1 := (Nat.succ_pred_eq_of_pos (card_pos_of_affineSpan_eq_top k V P h_tot)).symm
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
⊢ Fintype.card ι = finrank k V + 1
[PROOFSTEP]
rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot, ← hi.finrank_vectorSpan hn]
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ Fintype.card ι = finrank k V + 1 → affineSpan k (Set.range p) = ⊤
[PROOFSTEP]
intro hc
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k V + 1
⊢ affineSpan k (Set.range p) = ⊤
[PROOFSTEP]
rw [← finrank_top, ← direction_top k V P] at hc 
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
hc : Fintype.card ι = finrank k { x // x ∈ direction ⊤ } + 1
⊢ affineSpan k (Set.range p) = ⊤
[PROOFSTEP]
exact hi.affineSpan_eq_of_le_of_card_eq_finrank_add_one le_top hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
n : ℕ
T : Simplex k V n
hrank : finrank k V = n
⊢ affineSpan k (Set.range T.points) = ⊤
[PROOFSTEP]
rw [AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one T.Independent, Fintype.card_fin, hrank]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
⊢ FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
⊢ FiniteDimensional k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) }
[PROOFSTEP]
rcases(s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
[GOAL]
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
hs : ↑s = ∅
⊢ FiniteDimensional k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) }
[PROOFSTEP]
rw [coe_eq_bot_iff] at hs 
[GOAL]
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
hs : s = ⊥
⊢ FiniteDimensional k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) }
[PROOFSTEP]
rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan]
[GOAL]
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
hs : s = ⊥
⊢ FiniteDimensional k { x // x ∈ vectorSpan k (insert p ∅) }
[PROOFSTEP]
convert finiteDimensional_bot _ _
[GOAL]
case h.e'_2.h.e'_2.h.h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
hs : s = ⊥
x✝ : V
⊢ vectorSpan k (insert p ∅) = ⊥
[PROOFSTEP]
simp
[GOAL]
case h.e'_4.e'_6
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
hs : s = ⊥
e_2✝ : { x // x ∈ vectorSpan k (insert p ∅) } = { x // x ∈ ⊥ }
⊢ vectorSpan k (insert p ∅) = ⊥
[PROOFSTEP]
simp
[GOAL]
case h.e'_5.e'_6.h.h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p : P
hs : s = ⊥
e_2✝ : { x // x ∈ vectorSpan k (insert p ∅) } = { x // x ∈ ⊥ }
e_4✝ : HEq (Submodule.addCommGroup (vectorSpan k (insert p ∅))) (Submodule.addCommGroup ⊥)
e_3✝ : Ring.toSemiring = DivisionSemiring.toSemiring
⊢ vectorSpan k (insert p ∅) = ⊥
[PROOFSTEP]
simp
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ FiniteDimensional k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) }
[PROOFSTEP]
rw [affineSpan_coe, direction_affineSpan_insert hp₀]
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction s }
p p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ FiniteDimensional k { x // x ∈ Submodule.span k {p -ᵥ p₀} ⊔ direction s }
[PROOFSTEP]
infer_instance
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
p : P
⊢ FiniteDimensional k { x // x ∈ vectorSpan k (insert p s) }
[PROOFSTEP]
haveI : FiniteDimensional k (affineSpan k s).direction := (direction_affineSpan k s).symm ▸ inferInstance
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
p : P
this : FiniteDimensional k { x // x ∈ direction (affineSpan k s) }
⊢ FiniteDimensional k { x // x ∈ vectorSpan k (insert p s) }
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
p : P
this : FiniteDimensional k { x // x ∈ direction (affineSpan k s) }
⊢ FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑(affineSpan k s)) }
[PROOFSTEP]
exact finiteDimensional_vectorSpan_insert (affineSpan k s) p
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
[PROOFSTEP]
have h := collinear_iff_rank_le_one k s
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Collinear k s ↔ Module.rank k { x // x ∈ vectorSpan k s } ≤ 1
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
[PROOFSTEP]
rw [← finrank_eq_rank] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Collinear k s ↔ ↑(finrank k { x // x ∈ vectorSpan k s }) ≤ 1
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
[PROOFSTEP]
exact_mod_cast h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅
[PROOFSTEP]
rw [collinear_iff_rank_le_one, vectorSpan_empty]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Module.rank k { x // x ∈ ⊥ } ≤ 1
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ Collinear k {p}
[PROOFSTEP]
rw [collinear_iff_rank_le_one, vectorSpan_singleton]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ Module.rank k { x // x ∈ ⊥ } ≤ 1
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ Collinear k s ↔ ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
simp_rw [collinear_iff_rank_le_one, rank_submodule_le_one_iff', Submodule.le_span_singleton_iff]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ v₀, ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v) ↔ ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ v₀, ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v) → ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
rintro ⟨v₀, hv⟩
[GOAL]
case mp.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
⊢ ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
use v₀
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
⊢ ∀ (p : P), p ∈ s → ∃ r, p = r • v₀ +ᵥ p₀
[PROOFSTEP]
intro p hp
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
p : P
hp : p ∈ s
⊢ ∃ r, p = r • v₀ +ᵥ p₀
[PROOFSTEP]
obtain ⟨r, hr⟩ := hv (p -ᵥ p₀) (vsub_mem_vectorSpan k hp h)
[GOAL]
case h.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ ∃ r, p = r • v₀ +ᵥ p₀
[PROOFSTEP]
use r
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ p = r • v₀ +ᵥ p₀
[PROOFSTEP]
rw [eq_vadd_iff_vsub_eq]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ p -ᵥ p₀ = r • v₀
[PROOFSTEP]
exact hr.symm
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀) → ∃ v₀, ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
[PROOFSTEP]
rintro ⟨v, hp₀v⟩
[GOAL]
case mpr.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
⊢ ∃ v₀, ∀ (v : V), v ∈ vectorSpan k s → ∃ r, r • v₀ = v
[PROOFSTEP]
use v
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
⊢ ∀ (v_1 : V), v_1 ∈ vectorSpan k s → ∃ r, r • v = v_1
[PROOFSTEP]
intro w hw
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ ∃ r, r • v = w
[PROOFSTEP]
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
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ vectorSpan k s ≤ Submodule.span k {v}
[PROOFSTEP]
rw [vectorSpan_eq_span_vsub_set_right k h, Submodule.span_le, Set.subset_def]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ ∀ (x : V), x ∈ (fun x => x -ᵥ p₀) '' s → x ∈ ↑(Submodule.span k {v})
[PROOFSTEP]
intro x hx
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
x : V
hx : x ∈ (fun x => x -ᵥ p₀) '' s
⊢ x ∈ ↑(Submodule.span k {v})
[PROOFSTEP]
rw [SetLike.mem_coe, Submodule.mem_span_singleton]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
x : V
hx : x ∈ (fun x => x -ᵥ p₀) '' s
⊢ ∃ a, a • v = x
[PROOFSTEP]
rw [Set.mem_image] at hx 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
x : V
hx : ∃ x_1, x_1 ∈ s ∧ x_1 -ᵥ p₀ = x
⊢ ∃ a, a • v = x
[PROOFSTEP]
rcases hx with ⟨p, hp, rfl⟩
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
p : P
hp : p ∈ s
⊢ ∃ a, a • v = p -ᵥ p₀
[PROOFSTEP]
rcases hp₀v p hp with ⟨r, rfl⟩
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
r : k
hp : r • v +ᵥ p₀ ∈ s
⊢ ∃ a, a • v = r • v +ᵥ p₀ -ᵥ p₀
[PROOFSTEP]
use r
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
r : k
hp : r • v +ᵥ p₀ ∈ s
⊢ r • v = r • v +ᵥ p₀ -ᵥ p₀
[PROOFSTEP]
simp
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
hs : vectorSpan k s ≤ Submodule.span k {v}
⊢ ∃ r, r • v = w
[PROOFSTEP]
have hw' := SetLike.le_def.1 hs hw
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
hs : vectorSpan k s ≤ Submodule.span k {v}
hw' : w ∈ Submodule.span k {v}
⊢ ∃ r, r • v = w
[PROOFSTEP]
rwa [Submodule.mem_span_singleton] at hw' 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ Collinear k s ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
rcases Set.eq_empty_or_nonempty s with (rfl | ⟨⟨p₁, hp₁⟩⟩)
[GOAL]
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅ ↔ ∃ p₀ v, ∀ (p : P), p ∈ ∅ → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
simp [collinear_empty]
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
rw [collinear_iff_of_mem hp₁]
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁) ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
constructor
[GOAL]
case inr.intro.mp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁) → ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
exact fun h => ⟨p₁, h⟩
[GOAL]
case inr.intro.mpr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀) → ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
[PROOFSTEP]
rintro ⟨p, v, hv⟩
[GOAL]
case inr.intro.mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
⊢ ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
[PROOFSTEP]
use v
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
⊢ ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
[PROOFSTEP]
intro p₂ hp₂
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ r, p₂ = r • v +ᵥ p₁
[PROOFSTEP]
rcases hv p₂ hp₂ with ⟨r, rfl⟩
[GOAL]
case h.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ p₁
[PROOFSTEP]
rcases hv p₁ hp₁ with ⟨r₁, rfl⟩
[GOAL]
case h.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ (r₁ • v +ᵥ p)
[PROOFSTEP]
use r - r₁
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, 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)
[PROOFSTEP]
simp [vadd_vadd, ← add_smul]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ Collinear k {p₁, p₂}
[PROOFSTEP]
rw [collinear_iff_exists_forall_eq_smul_vadd]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ ∃ p₀ v, ∀ (p : P), p ∈ {p₁, p₂} → ∃ r, p = r • v +ᵥ p₀
[PROOFSTEP]
use p₁, p₂ -ᵥ p₁
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ ∀ (p : P), p ∈ {p₁, p₂} → ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
[PROOFSTEP]
intro p hp
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p ∈ {p₁, p₂}
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
[PROOFSTEP]
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp 
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁ ∨ p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
[PROOFSTEP]
cases' hp with hp hp
[GOAL]
case h.inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
[PROOFSTEP]
use 0
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ p = 0 • (p₂ -ᵥ p₁) +ᵥ p₁
[PROOFSTEP]
simp [hp]
[GOAL]
case h.inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
[PROOFSTEP]
use 1
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ p = 1 • (p₂ -ᵥ p₁) +ᵥ p₁
[PROOFSTEP]
simp [hp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
⊢ AffineIndependent k p ↔ ¬Collinear k (Set.range p)
[PROOFSTEP]
rw [collinear_iff_finrank_le_one, affineIndependent_iff_not_finrank_vectorSpan_le k p (Fintype.card_fin 3)]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
⊢ Collinear k (Set.range p) ↔ ¬AffineIndependent k p
[PROOFSTEP]
rw [collinear_iff_finrank_le_one, finrank_vectorSpan_le_iff_not_affineIndependent k p (Fintype.card_fin 3)]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
⊢ AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k {p₁, p₂, p₃}
[PROOFSTEP]
rw [affineIndependent_iff_not_collinear]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
⊢ ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k {p₁, p₂, p₃}
[PROOFSTEP]
simp_rw [Matrix.range_cons, Matrix.range_empty, Set.singleton_union, insert_emptyc_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}
[PROOFSTEP]
have hu : (Finset.univ : Finset (Fin 3)) = { i₁, i₂, i₃ } := by
  -- Porting note: Originally `by decide!`fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Finset.univ = {i₁, i₂, i₃}
[PROOFSTEP]
fin_cases i₁
[GOAL]
case head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ i₂
h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ i₃
⊢ Finset.univ = {{ val := 0, isLt := (_ : 0 < 3) }, i₂, i₃}
[PROOFSTEP]
fin_cases i₂
[GOAL]
case tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ i₂
h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ i₃
⊢ Finset.univ = {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, i₂, i₃}
[PROOFSTEP]
fin_cases i₂
[GOAL]
case tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₂ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ i₂
h₁₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ i₃
⊢ Finset.univ = {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, i₂, i₃}
[PROOFSTEP]
fin_cases i₂
[GOAL]
case head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ i₃
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ = {{ val := 0, isLt := (_ : 0 < 3) }, { val := 0, isLt := (_ : 0 < 3) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ i₃
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ i₃
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ = {{ val := 0, isLt := (_ : 0 < 3) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ i₃
h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ i₃
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ = {{ val := 0, isLt := (_ : 0 < 3) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ i₃
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ i₃
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ = {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 0, isLt := (_ : 0 < 3) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ i₃
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ = {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ i₃
h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ i₃
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case tail.tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ i₃
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ i₃
h₁₂ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ = {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 0, isLt := (_ : 0 < 3) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case tail.tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ i₃
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ i₃
h₁₂ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case tail.tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₃ : Fin 3
h₁₃ h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ i₃
h₁₂ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, i₃}
[PROOFSTEP]
fin_cases i₃
[GOAL]
case head.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 0, isLt := (_ : 0 < 3) }, { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₁₃ h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₁₃ h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.tail.tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.tail.tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case head.tail.tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₂₃ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 0, isLt := (_ : 0 < 3) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₁₃ h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₁₃ h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.tail.tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.tail.tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.head.tail.tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₂₃ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 1, isLt := (_ : (fun a => a < 3) 1) }, { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₁₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₁₃ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₂₃ : { val := 0, isLt := (_ : 0 < 3) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 0, isLt := (_ : 0 < 3) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₁₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
h₁₃ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₂₃ : { val := 1, isLt := (_ : (fun a => a < 3) 1) } ≠ { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.tail.tail.head.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₁₃ h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 0, isLt := (_ : 0 < 3) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 0, isLt := (_ : 0 < 3) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.tail.tail.head.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
h₁₃ h₂₃ : { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 3) 1) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }, { val := 1, isLt := (_ : (fun a => a < 3) 1) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
case tail.tail.head.tail.tail.head.tail.tail.head
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
h₁₂ h₁₃ h₂₃ :
  { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ≠
    { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
⊢ Finset.univ =
    {{ val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) },
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }}
[PROOFSTEP]
simp only at h₁₂ h₁₃ h₂₃ ⊢
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}
[PROOFSTEP]
rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu, Finset.coe_insert, Finset.coe_insert,
  Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₁ ≠ p₂
[PROOFSTEP]
rintro rfl
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₃ : P
h : ¬Collinear k {p₁, p₁, p₃}
⊢ False
[PROOFSTEP]
simp [collinear_pair] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₁ ≠ p₃
[PROOFSTEP]
rintro rfl
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₁}
⊢ False
[PROOFSTEP]
simp [collinear_pair] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₂ ≠ p₃
[PROOFSTEP]
rintro rfl
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₂}
⊢ False
[PROOFSTEP]
simp [collinear_pair] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ p₃ ∈ affineSpan k {p₁, p₂}
[PROOFSTEP]
rw [collinear_iff_of_mem hp₁] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h : ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ p₃ ∈ affineSpan k {p₁, p₂}
[PROOFSTEP]
rcases h with ⟨v, h⟩
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
⊢ p₃ ∈ affineSpan k {p₁, p₂}
[PROOFSTEP]
rcases h p₂ hp₂ with ⟨r₂, rfl⟩
[GOAL]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₃ : P
hp₁ : p₁ ∈ s
hp₃ : p₃ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
⊢ p₃ ∈ affineSpan k {p₁, r₂ • v +ᵥ p₁}
[PROOFSTEP]
rcases h p₃ hp₃ with ⟨r₃, rfl⟩
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ r₃ • v +ᵥ p₁ ∈ affineSpan k {p₁, r₂ • v +ᵥ p₁}
[PROOFSTEP]
rw [vadd_left_mem_affineSpan_pair]
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ ∃ r, r • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
[PROOFSTEP]
refine' ⟨r₃ / r₂, _⟩
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ (r₃ / r₂) • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
[PROOFSTEP]
have h₂ : r₂ ≠ 0 := by
  rintro rfl
  simp at hp₁p₂ 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ r₂ ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
hp₂ : 0 • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ 0 • v +ᵥ p₁
⊢ False
[PROOFSTEP]
simp at hp₁p₂ 
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
h₂ : r₂ ≠ 0
⊢ (r₃ / r₂) • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
[PROOFSTEP]
simp [smul_smul, h₂]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
[PROOFSTEP]
have hv : vectorSpan k (insert p₁ s) = vectorSpan k ({ p₁, p₂, p₃ } : Set P) := by
  -- Porting note: Original proof used `conv_lhs` and `conv_rhs`, but these tactics timed out.
  rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
  symm
  rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ direction (affineSpan k (insert p₁ ↑(affineSpan k s))) = vectorSpan k {p₁, p₂, p₃}
[PROOFSTEP]
symm
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ vectorSpan k {p₁, p₂, p₃} = direction (affineSpan k (insert p₁ ↑(affineSpan k s)))
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
⊢ Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
[PROOFSTEP]
rw [Collinear, Collinear, hv]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Collinear k (insert p s) ↔ Collinear k s
[PROOFSTEP]
rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₁, p₂, p₃}
[PROOFSTEP]
rw [collinear_insert_iff_of_mem_affineSpan h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₂, p₃}
[PROOFSTEP]
exact collinear_pair _ _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
h₁ : p₁ ∈ affineSpan k {p₃, p₄}
h₂ : p₂ ∈ affineSpan k {p₃, p₄}
⊢ Collinear k {p₁, p₂, p₃, p₄}
[PROOFSTEP]
rw [collinear_insert_iff_of_mem_affineSpan
    ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k (Set.subset_insert _ _)) _ h₁),
  collinear_insert_iff_of_mem_affineSpan h₂]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
h₁ : p₁ ∈ affineSpan k {p₃, p₄}
h₂ : p₂ ∈ affineSpan k {p₃, p₄}
⊢ Collinear k {p₃, p₄}
[PROOFSTEP]
exact collinear_pair _ _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₁, p₂, p₃, p₄, p₅}
[PROOFSTEP]
rw [collinear_insert_iff_of_mem_affineSpan
    ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k ((Set.subset_insert _ _).trans (Set.subset_insert _ _))) _ h₁),
  collinear_insert_iff_of_mem_affineSpan
    ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k (Set.subset_insert _ _)) _ h₂),
  collinear_insert_iff_of_mem_affineSpan h₃]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₄, p₅}
[PROOFSTEP]
exact collinear_pair _ _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₁, p₂, p₃, p₄}
[PROOFSTEP]
refine' (collinear_insert_insert_insert_of_mem_affineSpan_pair h₁ h₂ h₃).subset _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₁, p₂, p₃, p₄} ⊆ {p₁, p₂, p₃, p₄, p₅}
[PROOFSTEP]
repeat apply Set.insert_subset_insert
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₁, p₂, p₃, p₄} ⊆ {p₁, p₂, p₃, p₄, p₅}
[PROOFSTEP]
apply Set.insert_subset_insert
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₂, p₃, p₄} ⊆ {p₂, p₃, p₄, p₅}
[PROOFSTEP]
apply Set.insert_subset_insert
[GOAL]
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₃, p₄} ⊆ {p₃, p₄, p₅}
[PROOFSTEP]
apply Set.insert_subset_insert
[GOAL]
case h.h.h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₄} ⊆ {p₄, p₅}
[PROOFSTEP]
apply Set.insert_subset_insert
[GOAL]
case h.h.h
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₄} ⊆ {p₄, p₅}
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₁, p₂, p₃}
[PROOFSTEP]
refine' (collinear_insert_insert_insert_left_of_mem_affineSpan_pair h₁ h₂ h₃).subset _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₁, p₂, p₃} ⊆ {p₁, p₂, p₃, p₄}
[PROOFSTEP]
simp [Set.insert_subset_insert]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ FiniteDimensional k { x // x ∈ vectorSpan k s }
[PROOFSTEP]
refine' IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h _))
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ 2 < Cardinal.aleph0
[PROOFSTEP]
exact Cardinal.lt_aleph0.2 ⟨2, rfl⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
[PROOFSTEP]
have h : Coplanar k s ↔ Module.rank k (vectorSpan k s) ≤ 2 := Iff.rfl
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Coplanar k s ↔ Module.rank k { x // x ∈ vectorSpan k s } ≤ 2
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
[PROOFSTEP]
rw [← finrank_eq_rank] at h 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Coplanar k s ↔ ↑(finrank k { x // x ∈ vectorSpan k s }) ≤ 2
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
[PROOFSTEP]
exact_mod_cast h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Coplanar k (insert p s) ↔ Coplanar k s
[PROOFSTEP]
rw [Coplanar, Coplanar, vectorSpan_insert_eq_vectorSpan h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
by_cases hf : FiniteDimensional k s.direction
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
swap
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
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')
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
⊢ ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
[PROOFSTEP]
intro h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ False
[PROOFSTEP]
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 _ _)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ direction s ≤ vectorSpan k (insert p ↑s)
[PROOFSTEP]
conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
| direction s
[PROOFSTEP]
rw [← affineSpan_coe s, direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
| direction s
[PROOFSTEP]
rw [← affineSpan_coe s, direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
| direction s
[PROOFSTEP]
rw [← affineSpan_coe s, direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ vectorSpan k ↑s ≤ vectorSpan k (insert p ↑s)
[PROOFSTEP]
exact vectorSpan_mono k (Set.subset_insert _ _)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
h : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
h' : direction s ≤ vectorSpan k (insert p ↑s)
⊢ False
[PROOFSTEP]
exact hf (Submodule.finiteDimensional_of_le h')
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
hf' : ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
rw [finrank_of_infinite_dimensional hf, finrank_of_infinite_dimensional hf', zero_add]
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k { x // x ∈ direction s }
hf' : ¬FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
have : FiniteDimensional k s.direction := hf
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
rcases(s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
[GOAL]
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : ↑s = ∅
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
rw [coe_eq_bot_iff] at hs 
[GOAL]
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan, direction_bot, finrank_bot, zero_add]
[GOAL]
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } ≤ 1
[PROOFSTEP]
convert zero_le_one' ℕ
[GOAL]
case h.e'_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } = 0
[PROOFSTEP]
rw [← finrank_bot k V]
[GOAL]
case h.e'_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
⊢ finrank k { x // x ∈ vectorSpan k (insert p ∅) } = finrank k { x // x ∈ ⊥ }
[PROOFSTEP]
convert rfl
[GOAL]
case h.e'_3.h.e'_2.h.e'_2.h.h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
x✝ : V
⊢ ⊥ = vectorSpan k (insert p ∅)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_4.e'_6
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
e_2✝ : { x // x ∈ ⊥ } = { x // x ∈ vectorSpan k (insert p ∅) }
⊢ ⊥ = vectorSpan k (insert p ∅)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_5.e'_6
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
hs : s = ⊥
e_2✝ : { x // x ∈ ⊥ } = { x // x ∈ vectorSpan k (insert p ∅) }
e_3✝ : Ring.toSemiring = DivisionSemiring.toSemiring
e_4✝ : HEq (Submodule.addCommGroup ⊥) (Submodule.addCommGroup (vectorSpan k (insert p ∅)))
⊢ ⊥ = vectorSpan k (insert p ∅)
[PROOFSTEP]
simp
[GOAL]
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ direction (affineSpan k (insert p ↑(affineSpan k ↑s))) } ≤ finrank k { x // x ∈ direction s } + 1
[PROOFSTEP]
rw [affineSpan_coe, direction_affineSpan_insert hp₀, add_comm]
[GOAL]
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ Submodule.span k {p -ᵥ p₀} ⊔ direction s } ≤ 1 + finrank k { x // x ∈ direction s }
[PROOFSTEP]
refine' (Submodule.finrank_add_le_finrank_add_finrank _ _).trans (add_le_add_right _ _)
[GOAL]
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k { x // x ∈ Submodule.span k {p -ᵥ p₀} } ≤ 1
[PROOFSTEP]
refine' finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => _
[GOAL]
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
[PROOFSTEP]
have h := v.property
[GOAL]
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
h : ↑v ∈ Submodule.span k {p -ᵥ p₀}
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
[PROOFSTEP]
rw [Submodule.mem_span_singleton] at h 
[GOAL]
case pos.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
h : ∃ a, a • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
[PROOFSTEP]
rcases h with ⟨c, hc⟩
[GOAL]
case pos.inr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
[PROOFSTEP]
refine' ⟨c, _⟩
[GOAL]
case pos.inr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) } = v
[PROOFSTEP]
ext
[GOAL]
case pos.inr.intro.intro.a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf this : FiniteDimensional k { x // x ∈ direction s }
p₀ : P
hp₀ : p₀ ∈ ↑s
v : { x // x ∈ Submodule.span k {p -ᵥ p₀} }
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ↑(c • { val := p -ᵥ p₀, property := (_ : p -ᵥ p₀ ∈ Submodule.span k {p -ᵥ p₀}) }) = ↑v
[PROOFSTEP]
exact hc
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ vectorSpan k (insert p s) } ≤ finrank k { x // x ∈ vectorSpan k s } + 1
[PROOFSTEP]
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑(affineSpan k s)) } ≤ finrank k { x // x ∈ vectorSpan k s } + 1
[PROOFSTEP]
refine' (finrank_vectorSpan_insert_le _ _).trans (add_le_add_right _ _)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ direction (affineSpan k s) } ≤ finrank k { x // x ∈ vectorSpan k s }
[PROOFSTEP]
rw [direction_affineSpan]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
⊢ Coplanar k (insert p s)
[PROOFSTEP]
have : FiniteDimensional k { x // x ∈ vectorSpan k s } := h.finiteDimensional_vectorSpan
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ Coplanar k (insert p s)
[PROOFSTEP]
rw [coplanar_iff_finrank_le_two]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p s) } ≤ 2
[PROOFSTEP]
exact (finrank_vectorSpan_insert_le_set k s p).trans (add_le_add_right h.finrank_le_one _)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
⊢ Coplanar k s
[PROOFSTEP]
have : FiniteDimensional k V := finiteDimensional_of_finrank_eq_succ h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ Coplanar k s
[PROOFSTEP]
rw [coplanar_iff_finrank_le_two, ← h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ finrank k { x // x ∈ vectorSpan k s } ≤ finrank k V
[PROOFSTEP]
exact Submodule.finrank_le _
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
⊢ Nonempty (AffineBasis ι k P)
[PROOFSTEP]
obtain ⟨s, b, hb⟩ := AffineBasis.exists_affineBasis k V P
[GOAL]
case intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Set P
b : AffineBasis (↑s) k P
hb : ↑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)
[PROOFSTEP]
lift s to Finset P using b.finite_set
[GOAL]
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ↑b = Subtype.val
⊢ Nonempty (AffineBasis ι k P)
[PROOFSTEP]
refine' ⟨b.reindex <| Fintype.equivOfCardEq _⟩
[GOAL]
case intro.intro.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : DivisionRing k
inst✝² : Module k V
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional k V
h : Fintype.card ι = FiniteDimensional.finrank k V + 1
s : Finset P
b : AffineBasis (↑↑s) k P
hb : ↑b = Subtype.val
⊢ Fintype.card ↑↑s = Fintype.card ι
[PROOFSTEP]
rw [h, ← b.card_eq_finrank_add_one]
