-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
k : ℕ := #(minCardFinsetOfMemConvexHull (s := s) hx) - 1
hk : #(minCardFinsetOfMemConvexHull (s := s) hx) = k + 1
by_contra by_contra₁ by_contra₂ :
  ∀
    (h :
      ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
          (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx))),
    False
by_contra₃ :
  ∀
    (h :
      ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
          (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx)))
    (p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u))
    (hp :
      Membership.mem (γ := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
          Set E)
        x),
    False
by_contra₄ :
  ∀
    (h :
      ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
          (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx)))
    (p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u))
    (hp :
      Membership.mem (γ := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
          Set E)
        x)
    (contra :
      #(minCardFinsetOfMemConvexHull (s := s) hx) ≤ #((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E))),
    False
by_contra₅ :
  ∀
    (h :
      ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
          (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx)))
    (p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u))
    (hp :
      Membership.mem (γ := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
          Set E)
        x)
    (contra :
      ¬#((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) < #(minCardFinsetOfMemConvexHull (s := s) hx)),
    False
by_contra₆ :
  ∀
    (h :
      ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
          (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx)))
    (p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u))
    (hp :
      Membership.mem (γ := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
          Set E)
        x)
    (contra :
      ¬#((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) < #(minCardFinsetOfMemConvexHull (s := s) hx)),
    #((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) < #(minCardFinsetOfMemConvexHull (s := s) hx)
by_contra₇ :
  ∀
    (h :
      ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
          (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx)))
    (p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u))
    (hp :
      Membership.mem (γ := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
          Set E)
        x)
    (contra :
      ¬#((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) < #(minCardFinsetOfMemConvexHull (s := s) hx)),
    k + 1 - 1 < k + 1
⊢ AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
    (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx))

Tactic:
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
  rw [card_erase_of_mem p.2, hk]
  exact lt_add_one _

Premises used: lt_add_one, not_lt