awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
⊢ n ∈ {n} ∪ Set.range nj

Tactic:
simp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x ∈ {n} ∪ Set.range nj
refine_1 : Membership.mem (α := M) M' ((i : (a : ↥N) → M) x : M)
⊢ Membership.mem (α := M) M'
    (((↑↥A :
              {S M M₂ : Type u_1} →
                [inst_1 : Semiring ↥A] →
                  [inst_2 : Semiring S] →
                    [inst_3 : AddCommMonoid M] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : Module (↥A) M] →
                          [inst_6 : Module (↥A) M₂] →
                            [inst_7 : Module S M] →
                              [inst_8 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ (↥A) S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[↥A] M₂)
            i :
          (a : ↥N) → M)
        x :
      M)

Tactic:
change i x ∈ M'

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x ∈ {n} ∪ Set.range nj
⊢ x = n ∨ ∃ (y : Fin k), nj y = x

Tactic:
simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx

Premises used: Set.mem_range, Set.singleton_union, Set.mem_insert_iff
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n ∨ ∃ (y : Fin k), nj y = x
refine_1 : ∀ (hx : x = n), Membership.mem (α := M) M' ((i : (a : ↥N) → M) x : M)
refine_1₁ : ∀ (j : Fin k), Membership.mem (α := M) M' ((i : (a : ↥N) → M) (nj j) : M)
⊢ Membership.mem (α := M) M' ((i : (a : ↥N) → M) x : M)

Tactic:
rcases hx with hx | ⟨j, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n
refine_1 : ∑ i : Fin k, b i • mj i ∈ M'
⊢ Membership.mem (α := M) M' ((i : (a : ↥N) → M) x : M)

Tactic:
rw [hx, ← hb, piEquiv_apply_apply]

Premises used: Module.piEquiv_apply_apply
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n
⊢ ∑ i : Fin k, b i • mj i ∈ M'

Tactic:
Submodule.sum_mem _ fun j _ ↦ ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n
refine_1 : ∀ (j : Fin k), Membership.mem (γ := Finset (Fin k)) Finset.univ j → b j • mj j ∈ M'
⊢ ∑ i : Fin k, b i • mj i ∈ M'

Tactic:
refine Submodule.sum_mem _ fun j _ ↦ ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n
j : Fin k
h_1 : Membership.mem (γ := Finset (Fin k)) Finset.univ j
⊢ b j ∈ Set.range b ∪ Set.range (Function.uncurry c)

Tactic:
simp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n
j : Fin k
h_1 : Membership.mem (γ := Finset (Fin k)) Finset.univ j
b' : ↥A := Subtype.mk (p := fun (x : R) ↦ x ∈ A) (b j) ⋯
refine_1 : b' • mj j ∈ M'
⊢ b j • mj j ∈ M'

Tactic:
rw [show b j • mj j = b' • mj j from rfl]

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n
j : Fin k
h_1 : Membership.mem (γ := Finset (Fin k)) Finset.univ j
b' : ↥A := Subtype.mk (p := fun (x : R) ↦ x ∈ A) (b j) ⋯
⊢ mj j ∈ Set.range mj

Tactic:
simp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x_3 x : ↥N
hx : x = n
j : Fin k
h_1 : Membership.mem (γ := Finset (Fin k)) Finset.univ j
b' : ↥A := Subtype.mk (p := fun (x : R) ↦ x ∈ A) (b j) ⋯
⊢ b' • mj j ∈ M'

Tactic:
exact smul_mem _ _ (subset_span (by simp))

Premises used: Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x : ↥N
j : Fin k
refine_1 : ∑ i : Fin k, c j i • mj i ∈ M'
⊢ Membership.mem (α := M) M' ((i : (a : ↥N) → M) (nj j) : M)

Tactic:
rw [← hc, piEquiv_apply_apply]

Premises used: Module.piEquiv_apply_apply
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x_1 : AddCommMonoid M
x_2 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this_3 : IsNoetherianRing.{u_1} ↥A
this : Module.Finite.{u_1, u_1} ↥A ↥M'
x : ↥N
j : Fin k
⊢ ∑ i : Fin k, c j i • mj i ∈ M'

Tactic:
Submodule.sum_mem _ fun j' _ ↦ ?_

Premises used: Submodule.sum_mem