K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K Subtype.val) ↔
    ∃ s, Finset.card s = n ∧ LinearIndependent K Subtype.val
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
⊢ ↑n ≤ Module.rank K V ↔ ∃ s, Finset.card s = n ∧ LinearIndependent K Subtype.val
simp only [le_rank_iff_exists_linearIndependent, Cardinal.mk_set_eq_nat_iff_finset]
case mp
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K Subtype.val) →
    ∃ s, Finset.card s = n ∧ LinearIndependent K Subtype.val

case mpr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
⊢ (∃ s, Finset.card s = n ∧ LinearIndependent K Subtype.val) →
    ∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K Subtype.val
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K Subtype.val) ↔
    ∃ s, Finset.card s = n ∧ LinearIndependent K Subtype.val
constructor
case mp.intro.intro.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
t : Finset V
si : LinearIndependent K Subtype.val
⊢ ∃ s, Finset.card s = Finset.card t ∧ LinearIndependent K Subtype.val
case mp
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K Subtype.val) →
    ∃ s, Finset.card s = n ∧ LinearIndependent K Subtype.val
rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩
no goals
case mp.intro.intro.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
t : Finset V
si : LinearIndependent K Subtype.val
⊢ ∃ s, Finset.card s = Finset.card t ∧ LinearIndependent K Subtype.val
exact ⟨t, rfl, si⟩
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Finset V
si : LinearIndependent K Subtype.val
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ Finset.card t = Finset.card s) ∧ LinearIndependent K Subtype.val
case mpr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
⊢ (∃ s, Finset.card s = n ∧ LinearIndependent K Subtype.val) →
    ∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K Subtype.val
rintro ⟨s, rfl, si⟩
no goals
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1040875
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Finset V
si : LinearIndependent K Subtype.val
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ Finset.card t = Finset.card s) ∧ LinearIndependent K Subtype.val
exact ⟨s, ⟨s, rfl, rfl⟩, si⟩