-- Mathlib/RingTheory/Finiteness/TensorProduct.lean
lemma Module.exists_surjective_quotient_of_finite :
    ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I), I ≠ ⊤ ∧ Function.Surjective f

Proof state:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) x).quotKerEquivOfSurjective ⋯
e : LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x) = ⊤
⊢ False

Tactic:
obtain rfl : x = 0 := by simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1

Result:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : ⊤ = Submodule.span R {0}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0) = ⊤
⊢ False

Proof state:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : ⊤ = Submodule.span R {0}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0) = ⊤
⊢ False

Tactic:
rw [ne_eq, ← Submodule.subsingleton_quotient_iff_eq_top, ← not_nontrivial_iff_subsingleton,
  not_not] at hN

Result:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : Nontrivial (M ⧸ N)
hx : ⊤ = Submodule.span R {0}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0) = ⊤
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
⊢ Surjective ⇑(LinearMap.toSpanSingleton R (M ⧸ N) x)

Tactic:
rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx]

Result:
no goals

Proof state:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) x).quotKerEquivOfSurjective ⋯
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f

Tactic:
refine ⟨_, f.symm.toLinearMap.comp N.mkQ, fun e ↦ ?_, f.symm.surjective.comp N.mkQ_surjective⟩

Result:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) x).quotKerEquivOfSurjective ⋯
e : LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x) = ⊤
⊢ False

Proof state:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f

Tactic:
let f := (LinearMap.toSpanSingleton R _ x).quotKerEquivOfSurjective
  (by rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx])

Result:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) x).quotKerEquivOfSurjective ⋯
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) x).quotKerEquivOfSurjective ⋯
e : LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x) = ⊤
⊢ x = 0

Tactic:
simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f

Tactic:
obtain ⟨N, hN, ⟨x, hx⟩⟩ := Module.exists_isPrincipal_quotient_of_finite R M

Result:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = Submodule.span R {x}
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f

Proof state:
case intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : Nontrivial (M ⧸ N)
hx : ⊤ = Submodule.span R {0}
f : (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) 0) = ⊤
⊢ False

Tactic:
simp at hx

Result:
no goals