awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
x : ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
i : Fin n
hi : (f : (a : Fin n) → ι) i = (↑x : ι)
⊢ (↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) = (↑x : ι)

Tactic:
hi
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
x : ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
i : Fin n
hi : (f : (a : Fin n) → ι) i = (↑x : ι)
⊢ (↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) = (↑x : ι)

Tactic:
exact hi
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
⊢ Finset.univ = Finset.map f'' Finset.univ

Tactic:
have hu : (Finset.univ : Finset { x // x ∈ Finset.filter (fun x ↦ ∃ j, f j = x) Finset.univ }) =
      Finset.univ.map f'' := by
      ext x
      simp only [Finset.univ_eq_attach, Finset.mem_attach, Finset.mem_map, Finset.mem_univ,
        true_and, true_iff]
      have hx := x.property
      simp only [Finset.univ_filter_exists, Finset.mem_image, Finset.mem_univ, true_and] at hx
      rcases hx with ⟨i, hi⟩
      refine ⟨i, ?_⟩
      rw [Subtype.ext_iff]
      exact hi
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
e_a :
  Eq (α := ℕ)
    (∏ x : Fin n,
      AddSubgroup.index.{u_2} (G := R)
        (Submodule.toAddSubgroup
          (Ideal.span
            {a
                (⋯.choose (p := fun (j : Fin n) ↦
                  Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
                    ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) x) : ι) : ι)))})))
    (∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i})))
⊢ Eq (α := ℕ)
    (∏ x : ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x},
      AddSubgroup.index.{u_2} (G := R)
        (Submodule.toAddSubgroup
          (Ideal.span {a (⋯.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = (↑x : ι)))})))
    (∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i})))

Tactic:
rw [hu, Finset.prod_map]

Premises used: Finset.prod_map
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
e_a :
  ∀ (i : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ i →
      ⋯.choose (p := fun (j : Fin n) ↦
          Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
            ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι)) =
        i
⊢ Eq (α := ℕ)
    (∏ x : Fin n,
      AddSubgroup.index.{u_2} (G := R)
        (Submodule.toAddSubgroup
          (Ideal.span
            {a
                (⋯.choose (p := fun (j : Fin n) ↦
                  Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
                    ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) x) : ι) : ι)))})))
    (∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i})))

Tactic:
congr! with i
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
e_a :
  Eq (α := ι)
    ((f : (a : Fin n) → ι)
        (⋯.choose (p := fun (j : Fin n) ↦
          Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
            ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι))) :
      ι)
    ((f : (a : Fin n) → ι) i : ι)
⊢ ⋯.choose (p := fun (j : Fin n) ↦
      Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
        ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι)) =
    i

Tactic:
rw [← f.injective.eq_iff]

Premises used: Function.Injective.eq_iff, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
e_a :
  ∀
    (h :
      ∃ (j : Fin n),
        Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
          ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι)),
    Eq (α := ι)
      ((f : (a : Fin n) → ι)
          (h.choose (p := fun (j : Fin n) ↦
            Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
              ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι))) :
        ι)
      ((f : (a : Fin n) → ι) i : ι)
⊢ Eq (α := ι)
    ((f : (a : Fin n) → ι)
        (⋯.choose (p := fun (j : Fin n) ↦
          Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
            ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι))) :
      ι)
    ((f : (a : Fin n) → ι) i : ι)

Tactic:
generalize_proofs h
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
h :
  ∃ (j : Fin n),
    Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
      ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι)
e_a :
  Eq (α := ι) ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι)
    ((f : (a : Fin n) → ι) i : ι)
⊢ Eq (α := ι)
    ((f : (a : Fin n) → ι)
        (h.choose (p := fun (j : Fin n) ↦
          Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
            ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι))) :
      ι)
    ((f : (a : Fin n) → ι) i : ι)

Tactic:
rw [h.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
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)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN'_1 : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
hN' :
  Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))
f' : Fin n → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} :=
  fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : ι) ↦
      Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} x) ((f : (a : Fin n) → ι) i) ⋯
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
h :
  ∃ (j : Fin n),
    Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
      ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι)
⊢ Eq (α := ι) ((↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) : ι)
    ((f : (a : Fin n) → ι) i : ι)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Infinite R
inst_4 : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
rw :
  Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i})) =
    if n = Fintype.card ι then
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))
    else 0
⊢ N.toAddSubgroup.index =
    if n = Fintype.card ι then
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))
    else 0

Tactic:
rw [snf.toAddSubgroup_index_eq_pow_mul_prod]

Premises used: Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Infinite R
inst_4 : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
pos :
  ∀ (h : n = Fintype.card ι),
    Nat.card R ^ (Fintype.card ι - n) *
        ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i})) =
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))
neg :
  ∀ (h : ¬n = Fintype.card ι),
    Nat.card R ^ (Fintype.card ι - n) *
        ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i})) =
      0
⊢ Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i})) =
    if n = Fintype.card ι then
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))
    else 0

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Infinite R
inst_4 : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i})) =
    ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Infinite R
inst_4 : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
⊢ n ≤ Fintype.card ι

Tactic:
simpa using Fintype.card_le_of_embedding snf.f

Premises used: Module.Basis.SmithNormalForm.f, Fintype.card_le_of_embedding
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Infinite R
inst_4 : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
⊢ n < Fintype.card ι

Tactic:
have hlt : n < Fintype.card ι :=
      Ne.lt_of_le h (by simpa using Fintype.card_le_of_embedding snf.f)
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Infinite R
inst_4 : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
hlt : n < Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i})) =
    0

Tactic:
simp [hlt]
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
rw :
  Ne (α := ℕ)
      (if n = Fintype.card ι then
        ∏ i : Fin n, AddSubgroup.index (G := ℤ) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))
      else 0)
      0 ↔
    n = Fintype.card ι
⊢ N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι

Tactic:
rw [snf.toAddSubgroup_index_eq_ite]

Premises used: Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite