-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem lift_rank_range_le (f : M →ₗ[R] M') : Cardinal.lift.{v}
    (Module.rank R (LinearMap.range f)) ≤ Cardinal.lift.{v'} (Module.rank R M)

Proof state:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ LinearIndependent (ι := ↑(rangeSplitting ⇑f '' s)) R (⇑f.rangeRestrict ∘ fun x => id ↑x)

Tactic:
convert li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _) using 1

Result:
no goals

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
apply ciSup_le'

Result:
case h
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ∀ (i : { s // LinearIndepOn R id s }), lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Proof state:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ ?m.65965 ≤ ⨆ ι, #↑↑ι

R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ Cardinal.{v}

Tactic:
refine le_ciSup (Cardinal.bddAbove_range _) ⟨rangeSplitting f '' s, ?_⟩

Result:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ LinearIndepOn R id (rangeSplitting ⇑f '' s)

Proof state:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ LinearIndepOn R id (rangeSplitting ⇑f '' s)

Tactic:
apply LinearIndependent.of_comp f.rangeRestrict

Result:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ LinearIndependent (ι := ↑(rangeSplitting ⇑f '' s)) R (⇑f.rangeRestrict ∘ fun x => id ↑x)

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R ↥(LinearMap.range f)) ≤ lift.{v', v} (Module.rank R M)

Tactic:
simp only [Module.rank_def]

Result:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ lift.{v, v'} (⨆ ι, #↑↑ι) ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ lift.{v, v'} (⨆ ι, #↑↑ι) ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
rw [Cardinal.lift_iSup (Cardinal.bddAbove_range _)]

Result:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Proof state:
case h.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
apply le_trans

Result:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ ?h.mk.b

case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ ?h.mk.b ≤ lift.{v', v} (⨆ ι, #↑↑ι)

case h.mk.b
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ Cardinal.{max v' v}

Proof state:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ ?h.mk.b

case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ ?h.mk.b ≤ lift.{v', v} (⨆ ι, #↑↑ι)

case h.mk.b
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ Cardinal.{max v' v}

Tactic:
swap

Result:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ ?h.mk.b ≤ lift.{v', v} (⨆ ι, #↑↑ι)

case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ ?h.mk.b

case h.mk.b
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ Cardinal.{max v' v}

Proof state:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} #↑↑⟨rangeSplitting ⇑f '' s, ⋯⟩

Tactic:
exact (Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge

Result:
no goals

Proof state:
case h
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ∀ (i : { s // LinearIndepOn R id s }), lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
rintro ⟨s, li⟩

Result:
case h.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} (⨆ ι, #↑↑ι)