-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
/-- If an affine independent finset is contained in the affine span of another finset, then its
cardinality is at most the cardinality of that finset. -/
lemma AffineIndependent.card_le_card_of_subset_affineSpan {s t : Finset V}
    (hs : AffineIndependent k ((↑) : s → V)) (hst : (s : Set V) ⊆ affineSpan k (t : Set V)) :
    #s ≤ #t

Proof state:
case inr.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hs : AffineIndependent k Subtype.val
hs' : s.Nonempty
hst : ↑s ⊆ ↑(affineSpan k ↑∅)
⊢ #s ≤ #∅

Tactic:
simpa [Set.subset_empty_iff] using hst

Result:
no goals

Proof state:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : (affineSpan k ↑s).direction ≤ (affineSpan k ↑(affineSpan k ↑t)).direction
⊢ #s ≤ #t

Tactic:
rw [AffineSubspace.affineSpan_coe, direction_affineSpan, direction_affineSpan,
  ← @Subtype.range_coe _ (s : Set V), ← @Subtype.range_coe _ (t : Set V)] at direction_le

Result:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
⊢ #s ≤ #t

Proof state:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
finrank_le :
  finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s ≤ #t

Tactic:
erw [hs.finrank_vectorSpan_add_one] at finrank_le

Result:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
finrank_le : Fintype.card { x // x ∈ s } ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s ≤ #t

Proof state:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
⊢ #s ≤ #t

Tactic:
have direction_le := AffineSubspace.direction_le (affineSpan_mono k hst)

Result:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : (affineSpan k ↑s).direction ≤ (affineSpan k ↑(affineSpan k ↑t)).direction
⊢ #s ≤ #t

Proof state:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this : Nonempty { x // x ∈ s }
⊢ #s ≤ #t

Tactic:
have := ht'.to_set.to_subtype

Result:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
⊢ #s ≤ #t

Proof state:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
⊢ #s ≤ #t

Tactic:
have := hs'.to_subtype

Result:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this : Nonempty { x // x ∈ s }
⊢ #s ≤ #t

Proof state:
case inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑∅ ⊆ ↑(affineSpan k ↑t)
⊢ #∅ ≤ #t

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
⊢ #s ≤ #t

Tactic:
have finrank_le := add_le_add_right (Submodule.finrank_mono direction_le) 1

Result:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
finrank_le :
  finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s ≤ #t

Proof state:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty { x // x ∈ s }
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
finrank_le : Fintype.card { x // x ∈ s } ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s ≤ #t

Tactic:
simpa using finrank_le.trans <| finrank_vectorSpan_range_add_one_le _ _

Result:
no goals

Proof state:
case inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
⊢ #s ≤ #t

Tactic:
obtain rfl | ht' := t.eq_empty_or_nonempty

Result:
case inr.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hs : AffineIndependent k Subtype.val
hs' : s.Nonempty
hst : ↑s ⊆ ↑(affineSpan k ↑∅)
⊢ #s ≤ #∅

case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
⊢ #s ≤ #t

Proof state:
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
⊢ #s ≤ #t

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Result:
case inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑∅ ⊆ ↑(affineSpan k ↑t)
⊢ #∅ ≤ #t

case inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
⊢ #s ≤ #t