-- 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:
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 ⧸ 𝔪 • ⊤))
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
⊢ N = ⊤

Tactic:
have hf : Function.Surjective f := by
  intro x; obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
  rw [← this, LinearMap.comp_apply]; exact ⟨_, rfl⟩

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 ⧸ 𝔪 • ⊤))
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
⊢ 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
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))
⊢ N = ⊤

Tactic:
have : f.comp (TensorProduct.mk R k M 1) = Submodule.mkQ (𝔪 • ⊤) := by ext; simp [f]

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 ⧸ 𝔪 • ⊤))
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
⊢ 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
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 = ⊤

Tactic:
let f := AlgebraTensorModule.lift (((LinearMap.ringLmapEquivSelf k k _).symm
  (Submodule.mkQ (𝔪 • ⊤ : Submodule R M))).restrictScalars R)

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 ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
⊢ 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))
⊢ f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ

Tactic:
ext

Result:
case h
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))
x✝ : M
⊢ (f ∘ₗ (mk R k M) 1) x✝ = (𝔪 • ⊤).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
inst✝ : Module.Finite R M
⊢ Submodule.map ((mk R k M) 1) ⊤ = ⊤

Tactic:
rw [Submodule.map_top, LinearMap.range_eq_top]

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
⊢ Surjective ⇑((mk R k M) 1)

Proof state:
case h
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))
x✝ : M
⊢ (f ∘ₗ (mk R k M) 1) x✝ = (𝔪 • ⊤).mkQ x✝

Tactic:
simp [f]

Result:
no goals

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
inst✝ : Module.Finite R M
⊢ Surjective ⇑((mk R k M) 1)

Tactic:
exact TensorProduct.mk_surjective R M k Ideal.Quotient.mk_surjective

Result:
no goals

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 = (𝔪 • ⊤).mkQ x

Tactic:
rw [← this, LinearMap.comp_apply]

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 = f (((mk R k M) 1) x)