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.20136
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)
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.20136
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
⊢ A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)
set f : Submodule R B ≃o Set.Iic B := Submodule.MapSubtype.relIso B with hf
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.20136
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ IsCoatom { val := A, property := hAB } ↔
    IsCoatom (↑(Submodule.MapSubtype.relIso B) (Submodule.comap (Submodule.subtype B) A))
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.20136
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)
rw [covby_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]
no goals
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.20136
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ IsCoatom { val := A, property := hAB } ↔
    IsCoatom (↑(Submodule.MapSubtype.relIso B) (Submodule.comap (Submodule.subtype B) A))
simp [-OrderIso.isCoatom_iff, Submodule.MapSubtype.relIso, Submodule.map_comap_subtype,
  inf_eq_right.2 hAB]