-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem linearIndependent_bounded_of_finset_linearIndependent_bounded {n : ℕ}
    (H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) :
    ∀ s : Set M, LinearIndependent R ((↑) : s → M) → #s ≤ n

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ #↑s ≤ ↑n

Tactic:
apply Cardinal.card_le_of

Result:
case H
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), s_1.card ≤ n

Proof state:
case H
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), s_1.card ≤ n

Tactic:
intro t

Result:
case H
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ t.card ≤ n

Proof state:
case H
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ (Finset.map (Embedding.subtype s) t).card ≤ n

Tactic:
apply H

Result:
case H.a
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ LinearIndependent R fun i => ↑i

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
⊢ ∀ (s : Set M), LinearIndependent R Subtype.val → #↑s ≤ ↑n

Tactic:
intro s li

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ #↑s ≤ ↑n

Proof state:
case H
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ t.card ≤ n

Tactic:
rw [← Finset.card_map (Embedding.subtype s)]

Result:
case H
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ (Finset.map (Embedding.subtype s) t).card ≤ n

Proof state:
case H.a
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ LinearIndependent R fun i => ↑i

Tactic:
apply linearIndependent_finset_map_embedding_subtype _ li

Result:
no goals