-- 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:
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
⊢ Fin.val ⁻¹' Set.Iio x = Set.univ

Tactic:
ext y

Result:
case 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)) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
y : Fin n
⊢ y ∈ Fin.val ⁻¹' Set.Iio x ↔ y ∈ Set.univ

Proof state:
case 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
x✝ : ℕ
⊢ x✝ ∈ Set.Iio 0 ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
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, ⋯⟩}

Tactic:
simp [Fin.ext_iff]

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
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
⊢ 0 ∈ s

Tactic:
simp [s, show Set.Iio 0 = ∅ by ext; simp]

Result:
no goals

Proof state:
case 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)) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
y : Fin n
⊢ y ∈ Fin.val ⁻¹' Set.Iio x ↔ y ∈ Set.univ

Tactic:
simpa using y.2.trans_le e

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
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, ⋯⟩)}

Tactic:
rw [← Set.image_singleton, ← Submodule.map_span,
  ← (Submodule.comap_injective_of_surjective (Submodule.mkQ_surjective _)).eq_iff,
  Submodule.comap_map_eq, Submodule.ker_mkQ, Submodule.comap_top, ← this, ← Submodule.span_union,
  Order.Iio_succ_eq_insert (sSup s), ← Set.union_singleton, Set.preimage_union, Set.image_union,
  ← @Set.image_singleton _ _ f, Set.union_comm]

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 (f '' (Fin.val ⁻¹' {sSup s}) ∪ f '' (Fin.val ⁻¹' Set.Iio (sSup s))) =
    Submodule.span R (f '' {⟨sSup s, ⋯⟩} ∪ f '' (Fin.val ⁻¹' Set.Iio (sSup s)))

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 ∈ s, x < n

Tactic:
refine fun x hx ↦ lt_iff_not_le.mpr fun 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
⊢ 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)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
⊢ Set.Iio 0 = ∅

Tactic:
ext

Result:
case 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
x✝ : ℕ
⊢ x✝ ∈ Set.Iio 0 ↔ x✝ ∈ ∅

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
this : Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) = ⊤
⊢ Submodule.span R (f '' (Fin.val ⁻¹' {sSup s}) ∪ f '' (Fin.val ⁻¹' Set.Iio (sSup s))) =
    Submodule.span R (f '' {⟨sSup s, ⋯⟩} ∪ f '' (Fin.val ⁻¹' Set.Iio (sSup s)))

Tactic:
congr!

Result:
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, ⋯⟩}

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

Tactic:
have hs₁ : s.Nonempty := ⟨0, by simp [s, show Set.Iio 0 = ∅ by ext; simp]⟩

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