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}))
i : Fin n
⊢ Membership.mem (α := ι) (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
    ((f : (a : Fin n) → ι) i : ι)

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}))
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) ⋯
i j : Fin n
hij : f' i = f' j
⊢ (↑(f' i) : ι) = (↑(f' j) : ι)

Tactic:
rw [Subtype.ext_iff] at hij

Premises used: Subtype.ext_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'_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) ⋯
i j : Fin n
hij : (↑(f' i) : ι) = (↑(f' j) : ι)
⊢ i = j

Tactic:
f.injective hij

Premises used: 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) ⋯
i j : Fin n
hij : (↑(f' i) : ι) = (↑(f' j) : ι)
⊢ i = j

Tactic:
exact f.injective hij

Premises used: 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) ⋯
⊢ Function.Injective f'

Tactic:
have hf' : Function.Injective f' := fun i j hij ↦ by
      rw [Subtype.ext_iff] at hij
      exact f.injective hij
-- 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' }
h :
  ∀ (x : ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}),
    Membership.mem (γ := Finset ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) Finset.univ x ↔
      x ∈ Finset.map f'' Finset.univ
⊢ Finset.univ = Finset.map f'' Finset.univ

Tactic:
ext x
-- 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}
h : ∃ (a : Fin n), (f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) a = x
⊢ Membership.mem (γ := Finset ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) Finset.univ x ↔
    x ∈ Finset.map f'' Finset.univ

Tactic:
simp only [Finset.univ_eq_attach, Finset.mem_attach, Finset.mem_map, Finset.mem_univ,
        true_and, true_iff]

Premises used: Finset.mem_univ, true_iff, Finset.mem_attach, Finset.univ_eq_attach, Finset.mem_map, true_and
-- 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}
⊢ Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} (↑x : ι)

Tactic:
have hx := x.property
-- 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}
hx : Membership.mem (γ := Finset ι) {x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x} (↑x : ι)
⊢ ∃ (a : Fin n), (f : (a : Fin n) → ι) a = (↑x : ι)

Tactic:
simp only [Finset.univ_filter_exists, Finset.mem_image, Finset.mem_univ, true_and] at hx

Premises used: Finset.mem_univ, Finset.univ_filter_exists, Finset.mem_image, true_and
-- 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}
hx : ∃ (a : Fin n), (f : (a : Fin n) → ι) a = (↑x : ι)
h :
  ∀ (i : Fin n) (hi : (f : (a : Fin n) → ι) i = (↑x : ι)),
    ∃ (a : Fin n), (f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) a = x
⊢ ∃ (a : Fin n), (f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) a = x

Tactic:
rcases hx with ⟨i, 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 : ι)
⊢ ∃ (a : Fin n), (f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) a = x

Tactic:
⟨i, ?_⟩

Premises used: Exists.intro
-- 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 : ι)
h : (f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i = x
⊢ ∃ (a : Fin n), (f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) a = x

Tactic:
refine ⟨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' }
x : ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}
i : Fin n
hi : (f : (a : Fin n) → ι) i = (↑x : ι)
h : (↑((f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i) : ι) = (↑x : ι)
⊢ (f'' : (a : Fin n) → ↥{x : ι | ∃ (j : Fin n), (f : (a : Fin n) → ι) j = x}) i = x

Tactic:
rw [Subtype.ext_iff]

Premises used: Subtype.ext_iff