-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem le_rank_iff_exists_linearIndependent {c : Cardinal} {f : V →ₗ[K] V'} :
    c ≤ rank f ↔ ∃ s : Set V,
    Cardinal.lift.{v'} #s = Cardinal.lift.{v} c ∧ LinearIndepOn K f s

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
⊢ LinearIndependent (ι := ↑s) K (⇑(range f).subtype ∘ fun x => f.rangeRestrict ↑x)

Tactic:
convert si

Result:
no goals

Proof state:
case h.e'_3
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
this : LinearIndepOn K (⇑f.rangeRestrict) s
⊢ c = #↑(⇑f.rangeRestrict '' s)

Tactic:
rw [← Cardinal.lift_inj, ← hsc, Cardinal.mk_image_eq_of_injOn_lift]

Result:
case h.e'_3.h
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
this : LinearIndepOn K (⇑f.rangeRestrict) s
⊢ InjOn (⇑f.rangeRestrict) s

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥(range f)
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
fg : ∀ (x : ↥(range f)), f (g x) = ↑x
⊢ LinearIndepOn K (fun x => f (g x)) s

Tactic:
simpa only [fg] using si.map' _ (ker_subtype _)

Result:
no goals

Proof state:
case intro.refine_1.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥(range f)
h : #↑s ≤ f.rank
fg : ∀ (x : ↥(range f)), f (g x) = ↑x
si : LinearIndepOn K (fun x => f (g x)) s
⊢ LinearIndepOn K (⇑f) (⇑g '' s)

Tactic:
exact si.image_of_comp

Result:
no goals

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set ↥(range f)
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
⊢ ∀ (x : ↥(range f)), f (g x) = ↑x

Tactic:
intro x

Result:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set ↥(range f)
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
x : ↥(range f)
⊢ f (g x) = ↑x

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set ↥(range f)
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
x : ↥(range f)
⊢ f (g x) = ↑x

Tactic:
convert congr_arg Subtype.val (fg x)

Result:
no goals

Proof state:
case intro.refine_1.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥(range f)
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
fg : ∀ (x : ↥(range f)), f (g x) = ↑x
⊢ LinearIndepOn K (⇑f) (⇑g '' s)

Tactic:
replace si : LinearIndepOn K (fun x => f (g x)) s := by
  simpa only [fg] using si.map' _ (ker_subtype _)

Result:
case intro.refine_1.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥(range f)
h : #↑s ≤ f.rank
fg : ∀ (x : ↥(range f)), f (g x) = ↑x
si : LinearIndepOn K (fun x => f (g x)) s
⊢ LinearIndepOn K (⇑f) (⇑g '' s)

Proof state:
case intro.refine_2.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
⊢ c ≤ f.rank

Tactic:
have : LinearIndepOn K f.rangeRestrict s :=
  LinearIndependent.of_comp f.range.subtype (by convert si)

Result:
case intro.refine_2.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥(range f) →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
this : LinearIndepOn K (⇑f.rangeRestrict) s
⊢ c ≤ f.rank