-- Mathlib/RingTheory/Finiteness/TensorProduct.lean
lemma Module.exists_isPrincipal_quotient_of_finite  :
    ∃ N : Submodule R M, N ≠ ⊤ ∧ Submodule.IsPrincipal (⊤ : Submodule R (M ⧸ N))

Proof state:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
⊢ ⊤ = Submodule.span R {(Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio (sSup s)))).mkQ (f ⟨sSup s, ⋯⟩)}

Tactic:
have := not_not.mp (not_mem_of_csSup_lt (Order.lt_succ _) hs₂)

Result:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) = ⊤
⊢ ⊤ = Submodule.span R {(Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio (sSup s)))).mkQ (f ⟨sSup s, ⋯⟩)}

Proof state:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
let s := { m : ℕ | Submodule.span R (f '' (Fin.val ⁻¹' (Set.Iio m))) ≠ ⊤ }

Result:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Proof state:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
have hs₂ : BddAbove s := ⟨n, fun x hx ↦ (hns x hx).le⟩

Result:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
⊢ False

Tactic:
have : (Fin.val ⁻¹' Set.Iio x : Set (Fin n)) = Set.univ := by ext y; simpa using y.2.trans_le e

Result:
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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
this : Fin.val ⁻¹' Set.Iio x = Set.univ
⊢ 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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
this : Fin.val ⁻¹' Set.Iio x = Set.univ
⊢ False

Tactic:
simp [s, this, hf] at hx

Result:
no goals

Proof state:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
refine ⟨_, hs, ⟨⟨Submodule.mkQ _ (f ⟨_, hns _ hs⟩), ?_⟩⟩⟩

Result:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
⊢ ⊤ = Submodule.span R {(Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio (sSup s)))).mkQ (f ⟨sSup s, ⋯⟩)}

Proof state:
case intro.intro.h.e'_6.h.e'_3.h.e'_4
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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) = ⊤
⊢ Fin.val ⁻¹' {sSup s} = {⟨sSup s, ⋯⟩}

Tactic:
ext

Result:
case intro.intro.h.e'_6.h.e'_3.h.e'_4.h
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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) = ⊤
x✝ : Fin n
⊢ x✝ ∈ Fin.val ⁻¹' {sSup s} ↔ x✝ ∈ {⟨sSup s, ⋯⟩}

Proof state:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
have hns : ∀ x ∈ s, x < n := by
  refine fun x hx ↦ lt_iff_not_le.mpr fun e ↦ ?_
  have : (Fin.val ⁻¹' Set.Iio x : Set (Fin n)) = Set.univ := by ext y; simpa using y.2.trans_le e
  simp [s, this, hf] at hx

Result:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

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, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
obtain ⟨n, f, hf⟩ := @Module.Finite.exists_fin R M _ _ _ _

Result:
case intro.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 : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal