𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
⊢ AffineIndependent 𝕜 Subtype.val
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ AffineIndependent 𝕜 Subtype.val
let k := (minCardFinsetOfMemConvexHull hx).card - 1
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
⊢ AffineIndependent 𝕜 Subtype.val
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
⊢ AffineIndependent 𝕜 Subtype.val
have hk : (minCardFinsetOfMemConvexHull hx).card = k + 1 :=
  (Nat.succ_pred_eq_of_pos (Finset.card_pos.mpr (minCardFinsetOfMemConvexHull_nonempty hx))).symm
no goals
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
⊢ AffineIndependent 𝕜 Subtype.val
classical
by_contra h
obtain ⟨p, hp⟩ := mem_convexHull_erase h (mem_minCardFinsetOfMemConvexHull hx)
have contra := minCardFinsetOfMemConvexHull_card_le_card hx (Set.Subset.trans
  (Finset.erase_subset (p : E) (minCardFinsetOfMemConvexHull hx))
  (minCardFinsetOfMemConvexHull_subseteq hx)) hp
rw [← not_lt] at contra
apply contra
erw [card_erase_of_mem p.2, hk]
exact lt_add_one _
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
⊢ False
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
⊢ AffineIndependent 𝕜 Subtype.val
by_contra h
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
⊢ False
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
⊢ False
obtain ⟨p, hp⟩ := mem_convexHull_erase h (mem_minCardFinsetOfMemConvexHull hx)
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : card (minCardFinsetOfMemConvexHull hx) ≤ card (erase (minCardFinsetOfMemConvexHull hx) ↑p)
⊢ False
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
⊢ False
have contra := minCardFinsetOfMemConvexHull_card_le_card hx (Set.Subset.trans
  (Finset.erase_subset (p : E) (minCardFinsetOfMemConvexHull hx))
  (minCardFinsetOfMemConvexHull_subseteq hx)) hp
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ False
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : card (minCardFinsetOfMemConvexHull hx) ≤ card (erase (minCardFinsetOfMemConvexHull hx) ↑p)
⊢ False
rw [← not_lt] at contra
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ False
apply contra
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ k + 1 - 1 < k + 1
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
erw [card_erase_of_mem p.2, hk]
no goals
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜).toOrderHom ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ k + 1 - 1 < k + 1
exact lt_add_one _