-- Mathlib/LinearAlgebra/FreeModule/PID.lean
theorem Submodule.nonempty_basis_of_pid {ι : Type*} [Finite ι] (b : Basis ι R M)
    (N : Submodule R M) : ∃ n : ℕ, Nonempty (Basis (Fin n) R N)

Proof state:
case neg
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : ¬N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
obtain ⟨y, -, a, hay, M', -, N', N'_le_N, -, -, ay_ortho, h'⟩ :=
  Submodule.basis_of_pid_aux ⊤ N b' N_bot le_top

Result:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : ¬N = ⊥
y : M
a : R
hay : a • y ∈ N
M' N' : Submodule R M
N'_le_N : N' ≤ N
ay_ortho : ∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0
h' :
  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
    ∃ bN,
      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
        ∃ (hnm : n' + 1 ≤ m' + 1),
          ∃ bM,
            ∀ (as : Fin n' → R),
              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Proof state:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : ¬N = ⊥
y : M
a : R
hay : a • y ∈ N
M' N' : Submodule R M
N'_le_N : N' ≤ N
ay_ortho : ∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0
h' :
  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
    ∃ bN,
      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
        ∃ (hnm : n' + 1 ≤ m' + 1),
          ∃ bM,
            ∀ (as : Fin n' → R),
              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
obtain ⟨n', ⟨bN'⟩⟩ := ih N' N'_le_N _ hay ay_ortho

Result:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : ¬N = ⊥
y : M
a : R
hay : a • y ∈ N
M' N' : Submodule R M
N'_le_N : N' ≤ N
ay_ortho : ∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0
h' :
  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
    ∃ bN,
      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
        ∃ (hnm : n' + 1 ≤ m' + 1),
          ∃ bM,
            ∀ (as : Fin n' → R),
              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
n' : ℕ
bN' : Basis (Fin n') R ↥N'
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Proof state:
case intro.ih
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
let b' := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop _ rfl).symm

Result:
case intro.ih
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Proof state:
case intro.ih
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
by_cases N_bot : N = ⊥

Result:
case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

case neg
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : ¬N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Proof state:
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
N : Submodule R M
this : DecidableEq M
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
N : Submodule R M
this : DecidableEq M
val✝ : Fintype ι
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)