awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
⊢ ∃ (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)
have 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)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨m, b'M⟩ := M0.basisOfPid b
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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 : ℕ) (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)
have 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)
Tactic: by_cases N_bot : N = ⊥
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: by_cases N_bot : N = ⊥
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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 = ⊥
⊢ ∃ (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)
have 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)
Tactic: subst N_bot
Cleared hypotheses: N, N_le_O, N_bot
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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 = ⊥
⊢ ∃ (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)
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M'
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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 ι
⊢ ∃ (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)
have 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)
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⟩
Cleared hypotheses: N, O, N_le_O
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n
have 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
Tactic: choose n o hno bO bN a snf using N.exists_smith_normal_form_of_le b O N_le_O
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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)
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n
have 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)
Tactic: refine
    ⟨o, n, bO, bN.map (comapSubtypeEquivOfLe N_le_O).symm, (Fin.castLEEmb hno), a,
      fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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) =
    HSMul.hSMul (β := ↥O) (a i) ((bO : (a : Fin o) → ↥O) ((Fin.castLEEmb hno : (a : Fin n) → Fin o) i : Fin o) : ↥O)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
⊢ ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)
have intro : ∀ (val : Fintype ι),
  ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
val : Fintype ι
⊢ ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)
have intro : ∀ (bM : Basis ι R M) (bN : Basis.{0, u_2, u_3} (Fin (Fintype.card ι)) R ↥N) (f : Fin (Fintype.card ι) ↪ ι)
  (a : Fin (Fintype.card ι) → R)
  (snf :
    ∀ (i : Fin (Fintype.card ι)),
      (↑((bN : (a : Fin (Fintype.card ι)) → ↥N) i) : M) =
        HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin (Fintype.card ι)) → ι) i : ι) : M)),
  ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)
Tactic: let ⟨bM, bN, f, a, snf⟩ := N.smithNormalFormOfRankEq b h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
val : Fintype ι
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin (Fintype.card ι)) R ↥N
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf :
  ∀ (i : Fin (Fintype.card ι)),
    (↑((bN : (a : Fin (Fintype.card ι)) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin (Fintype.card ι)) → ι) i : ι) : M)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective (⇑f : (a : Fin (Fintype.card ι)) → ι) ⋯
⊢ ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)
have fe : ∀ (i : ι), (f : (a : Fin (Fintype.card ι)) → ι) ((e.symm : (a : ι) → Fin (Fintype.card ι)) i : Fin (Fintype.card ι)) = i
Tactic: have fe : ∀ i, f (e.symm i) = i := e.apply_symm_apply
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
i : ι
hi : smithNormalFormCoeffs b h i = 0
⊢ False
have apply : Eq.{u_3 + 1} (α := ↥N) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i : ↥N) (0 : ↥N)
Tactic: apply Basis.ne_zero (smithNormalFormBotBasis b h) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
i : ι
hi : smithNormalFormCoeffs b h i = 0
⊢ Eq.{u_3 + 1} (α := ↥N) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i : ↥N) (0 : ↥N)
have refine : Eq.{u_3 + 1} (α := M) ((fun (a : ↥N) ↦ (↑a : M)) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i))
  ((fun (a : ↥N) ↦ (↑a : M)) 0)
Tactic: refine Subtype.coe_injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S
have obtain : ∀ (fst : ℕ) (bS : Basis ι R S) (bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)) (f : Fin fst ↪ ι)
  (a : Fin fst → R),
  (∀ (i : Fin fst),
      (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
        HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)) →
    finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S
Tactic: obtain ⟨_, bS, bI, _, _, _⟩ := (I.restrictScalars R).smithNormalForm b
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst : ℕ
bS : Basis ι R S
bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)
f : Fin fst ↪ ι
a : Fin fst → R
snf :
  ∀ (i : Fin fst),
    (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
      HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)
⊢ finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S
have intro : ∀ (val : Fintype ι), finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S
Tactic: cases nonempty_fintype ι