-- Mathlib/RingTheory/Nakayama.lean
theorem sup_eq_sup_smul_of_le_smul_of_le_jacobson {I J : Ideal R} {N N' : Submodule R M}
    (hN' : N'.FG) (hIJ : I ≤ jacobson J) (hNN : N' ≤ N ⊔ I • N') : N ⊔ N' = N ⊔ J • N'

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
have hNN' : N ⊔ N' = N ⊔ I • N' :=
  le_antisymm (sup_le le_sup_left hNN)
  (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ map N.mkQ N' ≤ I • map N.mkQ N'

Tactic:
rw [← map_smul'', this]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
have :=
  @Submodule.eq_smul_of_le_smul_of_le_jacobson _ _ _ _ _ I J (N'.map N.mkQ) (hN'.map _)
    (by rw [← map_smul'', this]) hIJ

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
⊢ map N.mkQ (I • N') = map N.mkQ N'

Tactic:
simpa only [← h_comap.eq_iff, comap_map_mkQ, sup_comm, eq_comm] using hNN'

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
  sup_comm (b := N)] at this

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
have : (I • N').map N.mkQ = N'.map N.mkQ := by
  simpa only [← h_comap.eq_iff, comap_map_mkQ, sup_comm, eq_comm] using hNN'

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
have h_comap :=
  comap_injective_of_surjective (LinearMap.range_eq_top.1 N.range_mkQ)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
⊢ N ⊔ N' = N ⊔ J • N'