K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1195191
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 : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K fun x => ↑f ↑x) ↔
    ∃ s, Finset.card s = n ∧ LinearIndependent K fun x => ↑f ↑x
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1195191
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 : ℕ
f : V →ₗ[K] V'
⊢ ↑n ≤ rank f ↔ ∃ s, Finset.card s = n ∧ LinearIndependent K fun x => ↑f ↑x
simp only [le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff,
  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.1195191
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 : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K fun x => ↑f ↑x) →
    ∃ s, Finset.card s = n ∧ LinearIndependent K fun x => ↑f ↑x

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.1195191
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 : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, Finset.card s = n ∧ LinearIndependent K fun x => ↑f ↑x) →
    ∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K fun x => ↑f ↑x
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1195191
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 : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K fun x => ↑f ↑x) ↔
    ∃ s, Finset.card s = n ∧ LinearIndependent K fun x => ↑f ↑x
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.1195191
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
t : Finset V
si : LinearIndependent K fun x => ↑f ↑x
⊢ ∃ s, Finset.card s = Finset.card t ∧ LinearIndependent K fun x => ↑f ↑x
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.1195191
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 : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K fun x => ↑f ↑x) →
    ∃ s, Finset.card s = n ∧ LinearIndependent K fun x => ↑f ↑x
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.1195191
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
t : Finset V
si : LinearIndependent K fun x => ↑f ↑x
⊢ ∃ s, Finset.card s = Finset.card t ∧ LinearIndependent K fun x => ↑f ↑x
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.1195191
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
s : Finset V
si : LinearIndependent K fun x => ↑f ↑x
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ Finset.card t = Finset.card s) ∧ LinearIndependent K fun x => ↑f ↑x
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.1195191
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 : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, Finset.card s = n ∧ LinearIndependent K fun x => ↑f ↑x) →
    ∃ s, (∃ t, ↑t = s ∧ Finset.card t = n) ∧ LinearIndependent K fun x => ↑f ↑x
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.1195191
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
s : Finset V
si : LinearIndependent K fun x => ↑f ↑x
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ Finset.card t = Finset.card s) ∧ LinearIndependent K fun x => ↑f ↑x
exact ⟨s, ⟨s, rfl, rfl⟩, si⟩