-- Mathlib/LinearAlgebra/Isomorphisms.lean
theorem quotientInfEquivSupQuotient_surjective (p p' : Submodule R M) :
    Function.Surjective (quotientInfToSupQuotient p p')

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Surjective ⇑(quotientInfToSupQuotient p p')

Tactic:
rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ range (subToSupQuotient p p')

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ (inclusion ⋯) ⟨y, hy⟩ - ⟨y + z, hx⟩ ∈ comap (p ⊔ p').subtype p'

Tactic:
simp only [mem_comap, map_sub, coe_subtype, coe_inclusion, sub_add_cancel_left, neg_mem_iff, hz]

Result:
no goals

Proof state:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨x, hx⟩ ∈ range (subToSupQuotient p p')

Tactic:
rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩

Result:
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨y + z, hx⟩ ∈ range (subToSupQuotient p p')

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ (subToSupQuotient p p') ⟨y, hy⟩ = Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨y + z, hx⟩

Tactic:
apply (Submodule.Quotient.eq _).2

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ (inclusion ⋯) ⟨y, hy⟩ - ⟨y + z, hx⟩ ∈ comap (p ⊔ p').subtype p'

Proof state:
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨y + z, hx⟩ ∈ range (subToSupQuotient p p')

Tactic:
use ⟨y, hy⟩

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ (subToSupQuotient p p') ⟨y, hy⟩ = Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨y + z, hx⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ range (subToSupQuotient p p')

Tactic:
rintro ⟨x, hx⟩

Result:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨x, hx⟩ ∈ range (subToSupQuotient p p')