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' : 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
g : ι → R
h :
  ∀ (i : ι),
    (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) ∣
      g i
i : ι
hj : ∀ (j : Fin n), (f : (a : Fin n) → ι) j ≠ i
h₁ : 0 ∣ g i
⊢ g i = 0

Tactic:
rw [← zero_dvd_iff]

Premises used: zero_dvd_iff
-- 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' : 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
g : ι → R
h :
  ∀ (i : ι),
    (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) ∣
      g i
i : ι
hj : ∀ (j : Fin n), (f : (a : Fin n) → ι) j ≠ i
⊢ (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) ∣
    g i

Tactic:
h 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' : 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
g : ι → R
h :
  ∀ (i : ι),
    (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) ∣
      g i
i : ι
hj : ∀ (j : Fin n), (f : (a : Fin n) → ι) j ≠ i
h₁ :
  Eq.{u_2 + 1} (α := R) 0
    (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)
⊢ 0 ∣ g i

Tactic:
convert! h 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' : 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
g : ι → R
h :
  ∀ (i : ι),
    (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) ∣
      g i
i : ι
hj : ∀ (j : Fin n), (f : (a : Fin n) → ι) j ≠ i
⊢ Eq.{u_2 + 1} (α := R) 0
    (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)

Tactic:
simp [hj]
-- 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}))
simp :
  (∏ x ∈ Finset.attach {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 : ι)))}))) *
      Nat.card R ^ Finset.card.{u_1} (α := ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))
⊢ AddSubgroup.index (G := ι → R) N'.toAddSubgroup =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))

Tactic:
simp only [hN', AddSubgroup.index_pi, apply_dite, Finset.prod_dite, Set.singleton_zero,
    Ideal.span_zero, Submodule.bot_toAddSubgroup, AddSubgroup.index_pi, AddSubgroup.index_bot,
    Finset.prod_const, Finset.univ_eq_attach, Finset.card_attach]

Premises used: apply_dite, AddSubgroup.index_pi, Finset.prod_const, Finset.card_attach, Finset.univ_eq_attach, Ideal.span_zero, Finset.prod_dite, Submodule.bot_toAddSubgroup, AddSubgroup.index_bot, Set.singleton_zero
-- 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}))
rw :
  Nat.card R ^ Finset.card.{u_1} (α := ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} *
      ∏ x ∈ Finset.attach {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 : ι)))})) =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))
⊢ (∏ x ∈ Finset.attach {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 : ι)))}))) *
      Nat.card R ^ Finset.card.{u_1} (α := ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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}))
e_a : Finset.card.{u_1} (α := ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} = Fintype.card ι - n
e_a₁ :
  Eq (α := ℕ)
    (∏ x ∈ Finset.attach {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})))
⊢ Nat.card R ^ Finset.card.{u_1} (α := ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} *
      ∏ x ∈ Finset.attach {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 : ι)))})) =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))

Tactic:
congr
-- 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}))
⊢ Finset.card.{u_1} (α := ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}ᶜ =
    Fintype.card ι - Finset.card.{u_1} (α := ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}

Tactic:
Finset.card_compl {x | ∃ j, f j = x}

Premises used: Finset.univ, Finset.card_compl, Exists, Finset.filter, Eq, DFunLike.coe
-- 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}))
h :
  Eq.{u_1 + 1} (α := Finset ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
    {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}ᶜ
h₁ : n = Finset.card.{u_1} (α := ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
⊢ Finset.card.{u_1} (α := ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} = Fintype.card ι - n

Tactic:
convert! Finset.card_compl {x | ∃ j, f j = x} using 2

Premises used: Finset.univ, Finset.card_compl, Exists, Finset.filter, Eq, DFunLike.coe
-- 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}))
⊢ Eq.{u_1 + 1} (α := Finset ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
    {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}ᶜ

Tactic:
(Finset.compl_filter _).symm

Premises used: Finset.compl_filter, Eq.symm
-- 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}))
⊢ Eq.{u_1 + 1} (α := Finset ι) {x : ι | ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
    {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}ᶜ

Tactic:
exact (Finset.compl_filter _).symm

Premises used: Finset.compl_filter, Eq.symm
-- 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}))
⊢ Finset.card (α := Fin n) Finset.univ =
    Finset.card (α := ι) (Finset.image (α := Fin n) (⇑f : (a : Fin n) → ι) Finset.univ)

Tactic:
(Finset.card_image_of_injective Finset.univ f.injective).symm

Premises used: Finset.univ, Finset.card_image_of_injective, Function.Embedding.injective, Eq.symm
-- 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}))
h : n = Finset.card (α := Fin n) Finset.univ
h₁ :
  Eq (α := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
    (Finset.image (α := Fin n) (⇑f : (a : Fin n) → ι) Finset.univ)
⊢ n = Finset.card.{u_1} (α := ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}

Tactic:
convert! (Finset.card_image_of_injective Finset.univ f.injective).symm

Premises used: Finset.univ, Finset.card_image_of_injective, Function.Embedding.injective, Eq.symm
-- 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}))
⊢ n = Finset.card (α := Fin n) Finset.univ

Tactic:
simp
-- 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}))
⊢ Eq (α := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
    (Finset.image (α := Fin n) (⇑f : (a : Fin n) → ι) Finset.univ)

Tactic:
simp