R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ∀ (x : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'), x ∈ range (subToSupQuotient p p')
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ Function.Surjective ↑(quotientInfToSupQuotient p p')
rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']
case mk.mk
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := x, property := hx } ∈ range (subToSupQuotient p p')
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ∀ (x : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'), x ∈ range (subToSupQuotient p p')
rintro ⟨x, hx⟩
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := y + z, property := hx } ∈ range (subToSupQuotient p p')
case mk.mk
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := x, property := hx } ∈ range (subToSupQuotient p p')
rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(subToSupQuotient p p') { val := y, property := hy } = Quot.mk Setoid.r { val := y + z, property := hx }
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := y + z, property := hx } ∈ range (subToSupQuotient p p')
use ⟨y, hy⟩
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(ofLe (_ : p ≤ p ⊔ p')) { val := y, property := hy } - { val := y + z, property := hx } ∈
    comap (Submodule.subtype (p ⊔ p')) p'
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(subToSupQuotient p p') { val := y, property := hy } = Quot.mk Setoid.r { val := y + z, property := hx }
apply (Submodule.Quotient.eq _).2
no goals
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type ?u.65976
M₃ : Type ?u.65979
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(ofLe (_ : p ≤ p ⊔ p')) { val := y, property := hy } - { val := y + z, property := hx } ∈
    comap (Submodule.subtype (p ⊔ p')) p'
simp only [mem_comap, map_sub, coeSubtype, coe_ofLe, sub_add_cancel', neg_mem_iff, hz]