R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
⊢ x ∈ I • ⊤ ↔ ↑(Submodule.subtype N) x ∈ I • N
R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
⊢ x ∈ I • ⊤ ↔ ↑x ∈ I • N
change _ ↔ N.subtype x ∈ I • N
R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
this : map (Submodule.subtype N) (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ ↑(Submodule.subtype N) x ∈ I • N
R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
⊢ x ∈ I • ⊤ ↔ ↑(Submodule.subtype N) x ∈ I • N
have : Submodule.map N.subtype (I • ⊤) = I • N := by
  rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
this : map (Submodule.subtype N) (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ ↑(Submodule.subtype N) x ∈ map (Submodule.subtype N) (I • ⊤)
R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
this : map (Submodule.subtype N) (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ ↑(Submodule.subtype N) x ∈ I • N
rw [← this]
no goals
R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
this : map (Submodule.subtype N) (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ ↑(Submodule.subtype N) x ∈ map (Submodule.subtype N) (I • ⊤)
exact (Function.Injective.mem_set_image N.injective_subtype).symm
no goals
R : Type u
M : Type v
F : Type ?u.157879
G : Type ?u.157882
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
N : Submodule R M
x : { x // x ∈ N }
⊢ map (Submodule.subtype N) (I • ⊤) = I • N
rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]