-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_quotient_add_rank_le [Nontrivial R] (M' : Submodule R M) :
    Module.rank R (M ⧸ M') + Module.rank R M' ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

Tactic:
have := nonempty_linearIndependent_set R M'

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M

Tactic:
conv_lhs => simp only [Module.rank_def]

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
x✝¹ : { s // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x✝ : { s // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
⊢ #↑↑⟨s, hs⟩ + #↑↑⟨t, ht⟩ ≤ Module.rank R M

Tactic:
choose f hf using Submodule.Quotient.mk_surjective M'

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
x✝¹ : { s // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x✝ : { s // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
f : M ⧸ M' → M
hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b
⊢ #↑↑⟨s, hs⟩ + #↑↑⟨t, ht⟩ ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
x✝¹ : { s // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x✝ : { s // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
f : M ⧸ M' → M
hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b
⊢ LinearIndependent (ι := ↑s) R (Submodule.Quotient.mk ∘ fun i => f ↑i)

Tactic:
simpa [Function.comp_def, hf] using hs

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

Tactic:
have := nonempty_linearIndependent_set R (M ⧸ M')

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

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

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M

Tactic:
refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
x✝¹ : { s // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x✝ : { s // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
⊢ #↑↑⟨s, hs⟩ + #↑↑⟨t, ht⟩ ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
x✝¹ : { s // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x✝ : { s // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
f : M ⧸ M' → M
hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b
⊢ #↑↑⟨s, hs⟩ + #↑↑⟨t, ht⟩ ≤ Module.rank R M

Tactic:
simpa [add_comm] using (LinearIndependent.sumElim_of_quotient ht (fun (i : s) ↦ f i)
  (by simpa [Function.comp_def, hf] using hs)).cardinal_le_rank

Result:
no goals