case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.102423
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, X ⊔ Y).snd } ⧸ Submodule.comap (Submodule.subtype (X, X ⊔ Y).snd) (X, X ⊔ Y).fst) ≃ₗ[R]
    { x // x ∈ (X ⊓ Y, Y).snd } ⧸ Submodule.comap (Submodule.subtype (X ⊓ Y, Y).snd) (X ⊓ Y, Y).fst
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.102423
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ Iso (X, X ⊔ Y) (X ⊓ Y, Y)
constructor
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.102423
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, Y ⊔ X).snd } ⧸ Submodule.comap (Submodule.subtype (X, Y ⊔ X).snd) (X, Y ⊔ X).fst) ≃ₗ[R]
    { x // x ∈ (Y ⊓ X, Y).snd } ⧸ Submodule.comap (Submodule.subtype (Y ⊓ X, Y).snd) (Y ⊓ X, Y).fst
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.102423
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, X ⊔ Y).snd } ⧸ Submodule.comap (Submodule.subtype (X, X ⊔ Y).snd) (X, X ⊔ Y).fst) ≃ₗ[R]
    { x // x ∈ (X ⊓ Y, Y).snd } ⧸ Submodule.comap (Submodule.subtype (X ⊓ Y, Y).snd) (X ⊓ Y, Y).fst
rw [sup_comm, inf_comm]
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.102423
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ Y ⊔ X } ⧸ Submodule.comap (Submodule.subtype (Y ⊔ X)) X) ≃ₗ[R]
    { x // x ∈ Y } ⧸ Submodule.comap (Submodule.subtype Y) Y ⊓ Submodule.comap (Submodule.subtype Y) X
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.102423
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, Y ⊔ X).snd } ⧸ Submodule.comap (Submodule.subtype (X, Y ⊔ X).snd) (X, Y ⊔ X).fst) ≃ₗ[R]
    { x // x ∈ (Y ⊓ X, Y).snd } ⧸ Submodule.comap (Submodule.subtype (Y ⊓ X, Y).snd) (Y ⊓ X, Y).fst
dsimp
no goals
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type ?u.102423
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ Y ⊔ X } ⧸ Submodule.comap (Submodule.subtype (Y ⊔ X)) X) ≃ₗ[R]
    { x // x ∈ Y } ⧸ Submodule.comap (Submodule.subtype Y) Y ⊓ Submodule.comap (Submodule.subtype Y) X
exact (LinearMap.quotientInfEquivSupQuotient Y X).symm