-- Mathlib/RingTheory/LocalRing/Module.lean
theorem map_tensorProduct_mk_eq_top {N : Submodule R M} [Module.Finite R M] :
    N.map (TensorProduct.mk R k M 1) = ⊤ ↔ N = ⊤

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
⊢ Surjective ⇑f

Tactic:
intro x

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
x : M ⧸ 𝔪 • ⊤
⊢ ∃ a, f a = x

Proof state:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
⊢ N = ⊤

Tactic:
letI : IsScalarTower R k (M ⧸ (𝔪 • ⊤ : Submodule R M)) :=
  inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • (⊤ : Submodule R M)))

Result:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this✝ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
⊢ N = ⊤

Proof state:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map ((mk R k M) 1) N = ⊤ → N = ⊤

Tactic:
intro hN

Result:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
⊢ N = ⊤

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
x : M
⊢ ∃ a, f a = f (((mk R k M) 1) x)

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
hf : Surjective ⇑f
hN : Submodule.map f (Submodule.map ((mk R k M) 1) N) = Submodule.map f ⊤
⊢ N = ⊤

Tactic:
rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf,
  map_mkQ_eq_top] at hN

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
⊢ N = ⊤

Tactic:
letI : Module k (M ⧸ (𝔪 • ⊤ : Submodule R M)) :=
  inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • (⊤ : Submodule R M)))

Result:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
⊢ N = ⊤

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map ((mk R k M) 1) N = ⊤ ↔ N = ⊤

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map ((mk R k M) 1) N = ⊤ → N = ⊤

case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
⊢ N = ⊤ → Submodule.map ((mk R k M) 1) N = ⊤

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
x : M ⧸ 𝔪 • ⊤
⊢ ∃ a, f a = x

Tactic:
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x

Result:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
x : M
⊢ ∃ a, f a = (𝔪 • ⊤).mkQ x

Proof state:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
⊢ N = ⊤ → Submodule.map ((mk R k M) 1) N = ⊤

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
⊢ Submodule.map ((mk R k M) 1) ⊤ = ⊤