awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) N ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ N, Membership.mem (α := M) N ((f : (a : M) → M) x : M)
i : Fin n
⊢ (↑((f.restrict hf' : (a : ↥N) → ↥N) ((snf.bN : (a : Fin n) → ↥N) i)) : M) =
    (↑(HSMul.hSMul (β := ↥N) (snf.a i)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ N)
              ((f : (a : M) → M) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) i : ι) : M)) ⋯ :
            ↥N)) :
      M)

Tactic:
simp [snf.snf]

Premises used: Module.Basis.SmithNormalForm.snf
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
intro :
  ∀ (val : Fintype ι),
    ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥O) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
      Fin n → R),
      ∀ (i : Fin n),
        (↑((bN : (a : Fin n) → ↥N) i) : M) =
          HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥O) (Fin.castLE hno i)) : M)
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥O) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥O) (Fin.castLE hno i)) : M)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
val : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
          ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
            Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
            ∀ (i : Fin n),
              (↑((bN : (a : Fin n) → ↥N) i) : M) =
                HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M)
N : Submodule R M
N_le_O : N ≤ M0
intro :
  ∀ (m : ℕ) (b'M : Basis.{0, u_2, u_3} (Fin m) R ↥M0),
    ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a
      : Fin n → R),
      ∀ (i : Fin n),
        (↑((bN : (a : Fin n) → ↥N) i) : M) =
          HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)

Tactic:
obtain ⟨m, b'M⟩ := M0.basisOfPid b

Premises used: Submodule.basisOfPid
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
val : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
          ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
            Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
            ∀ (i : Fin n),
              (↑((bN : (a : Fin n) → ↥N) i) : M) =
                HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M)
N : Submodule R M
N_le_O : N ≤ M0
m : ℕ
b'M : Basis.{0, u_2, u_3} (Fin m) R ↥M0
pos :
  ∀ (N_bot : N = ⊥),
    ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a
      : Fin n → R),
      ∀ (i : Fin n),
        (↑((bN : (a : Fin n) → ↥N) i) : M) =
          HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)
neg :
  ∀ (N_bot : ¬N = ⊥),
    ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a
      : Fin n → R),
      ∀ (i : Fin n),
        (↑((bN : (a : Fin n) → ↥N) i) : M) =
          HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)

Tactic:
by_cases N_bot : N = ⊥
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
val : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
          ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
            Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
            ∀ (i : Fin n),
              (↑((bN : (a : Fin n) → ↥N) i) : M) =
                HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M)
N : Submodule R M
N_le_O : N ≤ M0
m : ℕ
b'M : Basis.{0, u_2, u_3} (Fin m) R ↥M0
N_bot : N = ⊥
pos :
  ∀ (N_le_O : ⊥ ≤ M0),
    ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥⊥) (a
      : Fin n → R),
      ∀ (i : Fin n),
        (↑((bN : (a : Fin n) → ↥⊥) i) : M) =
          HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)

Tactic:
subst N_bot
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
val : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
          ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
            Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
            ∀ (i : Fin n),
              (↑((bN : (a : Fin n) → ↥N) i) : M) =
                HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M)
m : ℕ
b'M : Basis.{0, u_2, u_3} (Fin m) R ↥M0
N_le_O : ⊥ ≤ M0
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥⊥) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥⊥) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)

Tactic:
⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩

Premises used: Nat.zero_le, finZeroElim, Exists.intro, Module.Basis.empty, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
val : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
          ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
            Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
            ∀ (i : Fin n),
              (↑((bN : (a : Fin n) → ↥N) i) : M) =
                HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M)
m : ℕ
b'M : Basis.{0, u_2, u_3} (Fin m) R ↥M0
N_le_O : ⊥ ≤ M0
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥⊥) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥⊥) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)

Tactic:
exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
val : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
          ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
            Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
            ∀ (i : Fin n),
              (↑((bN : (a : Fin n) → ↥N) i) : M) =
                HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M)
N : Submodule R M
N_le_O : N ≤ M0
m : ℕ
b'M : Basis.{0, u_2, u_3} (Fin m) R ↥M0
N_bot : ¬N = ⊥
neg :
  ∀ (y : M) (hy : y ∈ M0) (a : R),
    a • y ∈ N →
      ∀ (M' : Submodule R M) (M'_le_M : M' ≤ M0),
        ∀ N' ≤ N,
          ∀ (N'_le_M' : N' ≤ M') (y_ortho : ∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0),
            (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) →
              ∀
                (h :
                  ∀ (n' : ℕ) (bN' : Basis.{0, u_2, u_3} (Fin n') R ↥N'),
                    ∃ (bN : Basis.{0, u_2, u_3} (Fin (n' + 1)) R ↥N),
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis.{0, u_2, u_3} (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1) (bM : Basis.{0, u_2, u_3} (Fin (m' + 1)) R ↥M0),
                          ∀ (as : Fin n' → R),
                            (∀ (i : Fin n'),
                                (↑((bN' : (a : Fin n') → ↥N') i) : M) =
                                  HSMul.hSMul (β := M) (as i)
                                    (↑((bM' : (a : Fin m') → ↥M') (Fin.castLE hn'm' i)) : M)) →
                              ∃ (as' : Fin (n' + 1) → R),
                                ∀ (i : Fin (n' + 1)),
                                  (↑((bN : (a : Fin (n' + 1)) → ↥N) i) : M) =
                                    HSMul.hSMul (β := M) (as' i)
                                      (↑((bM : (a : Fin (m' + 1)) → ↥M0) (Fin.castLE hnm i)) : M)),
                ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN :
                  Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
                  ∀ (i : Fin n),
                    (↑((bN : (a : Fin n) → ↥N) i) : M) =
                      HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)

Tactic:
obtain ⟨y, hy, a, _, M', M'_le_M, N', _, N'_le_M', y_ortho, _, h⟩ :=
    Submodule.basis_of_pid_aux M0 N b'M N_bot N_le_O

Premises used: Submodule.basis_of_pid_aux
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
val : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
          ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
            Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
            ∀ (i : Fin n),
              (↑((bN : (a : Fin n) → ↥N) i) : M) =
                HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M)
N : Submodule R M
N_le_O : N ≤ M0
m : ℕ
b'M : Basis.{0, u_2, u_3} (Fin m) R ↥M0
N_bot : ¬N = ⊥
y : M
hy : y ∈ M0
a : R
left : a • y ∈ N
M' : Submodule R M
M'_le_M : M' ≤ M0
N' : Submodule R M
left_1 : N' ≤ N
N'_le_M' : N' ≤ M'
y_ortho : ∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0
left_2 : ∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0
h :
  ∀ (n' : ℕ) (bN' : Basis.{0, u_2, u_3} (Fin n') R ↥N'),
    ∃ (bN : Basis.{0, u_2, u_3} (Fin (n' + 1)) R ↥N),
      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis.{0, u_2, u_3} (Fin m') R ↥M'),
        ∃ (hnm : n' + 1 ≤ m' + 1) (bM : Basis.{0, u_2, u_3} (Fin (m' + 1)) R ↥M0),
          ∀ (as : Fin n' → R),
            (∀ (i : Fin n'),
                (↑((bN' : (a : Fin n') → ↥N') i) : M) =
                  HSMul.hSMul (β := M) (as i) (↑((bM' : (a : Fin m') → ↥M') (Fin.castLE hn'm' i)) : M)) →
              ∃ (as' : Fin (n' + 1) → R),
                ∀ (i : Fin (n' + 1)),
                  (↑((bN : (a : Fin (n' + 1)) → ↥N) i) : M) =
                    HSMul.hSMul (β := M) (as' i) (↑((bM : (a : Fin (m' + 1)) → ↥M0) (Fin.castLE hnm i)) : M)
neg :
  ∀ (n' m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis.{0, u_2, u_3} (Fin m') R ↥M') (bN' : Basis.{0, u_2, u_3} (Fin n') R ↥N')
    (as' : Fin n' → R)
    (has' :
      ∀ (i : Fin n'),
        (↑((bN' : (a : Fin n') → ↥N') i) : M) =
          HSMul.hSMul (β := M) (as' i) (↑((bM' : (a : Fin m') → ↥M') (Fin.castLE hn'm' i)) : M)),
    ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a
      : Fin n → R),
      ∀ (i : Fin n),
        (↑((bN : (a : Fin n) → ↥N) i) : M) =
          HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)

Tactic:
obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M'
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
val : Fintype ι
intro :
  ∀ (M0 : Submodule R M)
    (ih :
      ∀ N' ≤ M0,
        ∀ x ∈ M0,
          (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
            ∀ (N : Submodule R M) (N_le_O : N ≤ N'),
              ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥N') (bN :
                Basis.{0, u_2, u_3} (Fin n) R ↥N) (a : Fin n → R),
                ∀ (i : Fin n),
                  (↑((bN : (a : Fin n) → ↥N) i) : M) =
                    HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥N') (Fin.castLE hno i)) : M))
    (N : Submodule R M) (N_le_O : N ≤ M0),
    ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥M0) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a
      : Fin n → R),
      ∀ (i : Fin n),
        (↑((bN : (a : Fin n) → ↥N) i) : M) =
          HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥M0) (Fin.castLE hno i)) : M)
⊢ ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Basis.{0, u_2, u_3} (Fin o) R ↥O) (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) (a :
    Fin n → R),
    ∀ (i : Fin n),
      (↑((bN : (a : Fin n) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥O) (Fin.castLE hno i)) : M)

Tactic:
induction O using inductionOnRank b generalizing N with | ih M0 ih =>
  obtain ⟨m, b'M⟩ := M0.basisOfPid b
  by_cases N_bot : N = ⊥
  · subst N_bot
    exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩
  obtain ⟨y, hy, a, _, M', M'_le_M, N', _, N'_le_M', y_ortho, _, h⟩ :=
    Submodule.basis_of_pid_aux M0 N b'M N_bot N_le_O
  obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M'
  obtain ⟨bN, h'⟩ := h n' bN'
  obtain ⟨hmn, bM, h''⟩ := h' m' hn'm' bM'
  obtain ⟨as, has⟩ := h'' as' has'
  exact ⟨_, _, hmn, bM, bN, as, has⟩

Premises used: Submodule.inductionOnRank
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b_1 : ι → M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
choose :
  (n o : ℕ) →
    (hno : n ≤ o) →
      (bO : Basis.{0, u_2, u_3} (Fin o) R ↥O) →
        (bN : Basis.{0, u_2, u_3} (Fin n) R ↥N) →
          (a : Fin n → R) →
            (snf :
                ∀ (i : Fin n),
                  (↑((bN : (a : Fin n) → ↥N) i) : M) =
                    HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥O) (Fin.castLE hno i)) : M)) →
              (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n

Tactic:
choose n o hno bO bN a snf using N.exists_smith_normal_form_of_le b O N_le_O

Premises used: Submodule.exists_smith_normal_form_of_le
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b_1 : ι → M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
n o : ℕ
hno : n ≤ o
bO : Basis.{0, u_2, u_3} (Fin o) R ↥O
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥O) (Fin.castLE hno i)) : M)
fun :
  ∀ (i : Fin n),
    (↑((bN.map (comapSubtypeEquivOfLe N_le_O).symm : (a : Fin n) → ↥(comap O.subtype N)) i) : ↥O) =
      HSMul.hSMul (β := ↥O) (a i) ((bO : (a : Fin o) → ↥O) ((Fin.castLEEmb hno : (a : Fin n) → Fin o) i : Fin o) : ↥O)
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n

Tactic:
refine
    ⟨o, n, bO, bN.map (comapSubtypeEquivOfLe N_le_O).symm, (Fin.castLEEmb hno), a,
      fun i ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b_1 : ι → M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
n o : ℕ
hno : n ≤ o
bO : Basis.{0, u_2, u_3} (Fin o) R ↥O
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥O) (Fin.castLE hno i)) : M)
i : Fin n
a₁ :
  (↑(↑((bN.map (comapSubtypeEquivOfLe N_le_O).symm : (a : Fin n) → ↥(comap O.subtype N)) i) : ↥O) : M) =
    (↑(HSMul.hSMul (β := ↥O) (a i)
          ((bO : (a : Fin o) → ↥O) ((Fin.castLEEmb hno : (a : Fin n) → Fin o) i : Fin o) : ↥O)) :
      M)
⊢ (↑((bN.map (comapSubtypeEquivOfLe N_le_O).symm : (a : Fin n) → ↥(comap O.subtype N)) i) : ↥O) =
    HSMul.hSMul (β := ↥O) (a i) ((bO : (a : Fin o) → ↥O) ((Fin.castLEEmb hno : (a : Fin n) → Fin o) i : Fin o) : ↥O)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b_1 : ι → M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
n o : ℕ
hno : n ≤ o
bO : Basis.{0, u_2, u_3} (Fin o) R ↥O
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) (↑((bO : (a : Fin o) → ↥O) (Fin.castLE hno i)) : M)
i : Fin n
⊢ (↑(↑((bN.map (comapSubtypeEquivOfLe N_le_O).symm : (a : Fin n) → ↥(comap O.subtype N)) i) : ↥O) : M) =
    (↑(HSMul.hSMul (β := ↥O) (a i)
          ((bO : (a : Fin o) → ↥O) ((Fin.castLEEmb hno : (a : Fin n) → Fin o) i : Fin o) : ↥O)) :
      M)

Tactic:
simp only [snf, Basis.map_apply, Submodule.comapSubtypeEquivOfLe_symm_apply,
    Submodule.coe_smul_of_tower, Fin.castLEEmb_apply]

Premises used: Module.Basis.map_apply, Submodule.coe_smul_of_tower, Submodule.comapSubtypeEquivOfLe_symm_apply, Fin.castLEEmb_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b_1 : ι → M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
b : Basis ι R M
N : Submodule R M
m n : ℕ
bM : Basis.{0, u_2, u_3} (Fin m) R ↥⊤
bN : Basis.{0, u_2, u_3} (Fin n) R ↥(comap (Submodule.subtype ⊤) N)
f : Fin n ↪ Fin m
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥(comap ⊤.subtype N)) i) : ↥⊤) =
      HSMul.hSMul (β := ↥⊤) (a i) ((bM : (a : Fin m) → ↥⊤) ((f : (a : Fin n) → Fin m) i : Fin m) : ↥⊤)
bM' : Basis (Fin m) R M := bM.map (LinearEquiv.ofTop ⊤ ⋯)
e : Fin m ≃ ι := bM'.indexEquiv b
i : Fin n
⊢ (↑((bN.map (comapSubtypeEquivOfLe ⋯) : (a : Fin n) → ↥N) i) : M) =
    HSMul.hSMul (β := M) (a i) ((bM'.reindex e : (a : ι) → M) ((f.trans e.toEmbedding : (a : Fin n) → ι) i : ι) : M)

Tactic:
simp only [bM', snf, Basis.map_apply, LinearEquiv.ofTop_apply, Submodule.coe_smul_of_tower,
      Submodule.comapSubtypeEquivOfLe_apply_coe, Basis.reindex_apply,
      Equiv.toEmbedding_apply, Function.Embedding.trans_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Equiv.toEmbedding_apply, Function.Embedding.trans_apply, Module.Basis.map_apply, Submodule.coe_smul_of_tower, Submodule.comapSubtypeEquivOfLe_apply_coe, LinearEquiv.ofTop_apply, Module.Basis.reindex_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b_1 : ι → M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Fintype ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
n : ℕ
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
⊢ Fintype.card (Fin n) = Fintype.card (Fin (Fintype.card ι))

Tactic:
simp only [Fintype.card_fin, ← Module.finrank_eq_card_basis bM, ← h,
      Module.finrank_eq_card_basis bN]

Premises used: Fintype.card_fin, Module.finrank_eq_card_basis
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b_1 : ι → M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Fintype ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
n : ℕ
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
e : Fin n ≃ Fin (Fintype.card ι) := Fintype.equivOfCardEq ⋯
i : Fin (Fintype.card ι)
⊢ (↑((bN.reindex e : (a : Fin (Fintype.card ι)) → ↥N) i) : M) =
    HSMul.hSMul (β := M) ((a ∘ (⇑e.symm : (a : Fin (Fintype.card ι)) → Fin n)) i)
      ((bM : (a : ι) → M) ((e.symm.toEmbedding.trans f : (a : Fin (Fintype.card ι)) → ι) i : ι) : M)

Tactic:
simp only [snf, Basis.coe_reindex, Function.Embedding.trans_apply, Equiv.toEmbedding_apply,
      (· ∘ ·)]

Premises used: Function.comp, Equiv.toEmbedding_apply, Function.Embedding.trans_apply, Module.Basis.coe_reindex