awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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
⊢ Membership.mem (α := M) M' ((i : (a : ↥N) → M) (nj j) : M)
have refine_1 : ∑ i : Fin k, c j i • mj i ∈ M'
Tactic: rw [← hc, piEquiv_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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'
have refine_1 : ∀ (j' : Fin k), Membership.mem (γ := Finset (Fin k)) Finset.univ j' → c j j' • mj j' ∈ M'
Tactic: refine Submodule.sum_mem _ fun j' _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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 j' : Fin k
h_1 : Membership.mem (γ := Finset (Fin k)) Finset.univ j'
c' : ↥A := Subtype.mk (p := fun (x : R) ↦ x ∈ A) (c j j') ⋯
⊢ c j j' • mj j' ∈ M'
have refine_1 : c' • mj j' ∈ M'
Tactic: rw [show c j j' • mj j' = c' • mj j' from rfl]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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
⊢ 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₂)
            f :
          (a : ↥N) → M)
        x :
      M)
have refine_2 : Membership.mem (α := M) M' ((f : (a : ↥N) → M) x : M)
Tactic: change f x ∈ M'
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
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
⊢ Membership.mem (α := M) M' ((f : (a : ↥N) → M) x : M)
have hx₁ : x = n ∨ ∃ (y : Fin k), nj y = x
Tactic: simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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
⊢ Membership.mem (α := M) M' ((f : (a : ↥N) → M) x : M)
have refine_2 : ∀ (hx : x = n), Membership.mem (α := M) M' ((f : (a : ↥N) → M) x : M)
Tactic: rcases hx with hx | ⟨j, rfl⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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_2 : ∀ (hx : x = n), Membership.mem (α := M) M' ((f : (a : ↥N) → M) x : M)
⊢ Membership.mem (α := M) M' ((f : (a : ↥N) → M) x : M)
have refine_2₁ : ∀ (j : Fin k), Membership.mem (α := M) M' ((f : (a : ↥N) → M) (nj j) : M)
Tactic: rcases hx with hx | ⟨j, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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
⊢ Membership.mem (α := M) M' ((f : (a : ↥N) → M) x : M)
have refine_2 : 0 ∈ M'
Tactic: rw [hx, hn]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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 : ↥M'
x : M
hx : x ∈ M'
⊢ ∃ (a : ↥N'),
    (LinearMap.restrict
            ((↑↥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₂)
              f)
            ⋯ :
          (a : ↥N') → ↥M')
        a =
      Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx
have refine_3 : Membership.mem (γ := Submodule (↥A) M)
  (LinearMap.range
    (LinearMap.domRestrict
      ((↑↥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₂)
        f)
      N'))
  x
Tactic: suffices x ∈ LinearMap.range ((f.restrictScalars A).domRestrict N') by
    obtain ⟨a, ha⟩ := this
    exact ⟨a, Subtype.val_injective ha⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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 : ↥M'
x_4 x : M
hx : x ∈ Set.range mj
⊢ Membership.mem (γ := Submodule (↥A) M)
    (LinearMap.range
      (LinearMap.domRestrict
        ((↑↥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₂)
          f)
        N'))
    x
have refine_3 : ∀ (j : Fin k),
  Membership.mem (γ := Submodule (↥A) M)
    (LinearMap.range
      (LinearMap.domRestrict
        ((↑↥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₂)
          f)
        N'))
    (mj j)
Tactic: obtain ⟨j, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R M) (span R (↑∅ : Set M)) ⊥
have rw : Eq.{u_2 + 1} (α := Submodule R M) (span R ∅) ⊥
Tactic: rw [Finset.coe_empty, span_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : Eq.{u_2 + 1} (α := Submodule R M) (span R ∅) ⊥
⊢ Eq (α := Submodule R M) (span R (↑∅ : Set M)) ⊥
have rw₁ : Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊥
Tactic: rw [Finset.coe_empty, span_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
hs : s.Finite
⊢ Eq (α := Submodule R M) (span R (↑(hs.toFinset (s := s)) : Set M)) (span R s)
have rw : Eq (α := Submodule R M) (span R s) (span R s)
Tactic: rw [hs.coe_toFinset]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw : span R t₁ ⊔ span R t₂ = N₁ ⊔ N₂
Tactic: rw [span_union, span_t₁, span_t₂]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
rw : span R t₁ ⊔ span R t₂ = N₁ ⊔ N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw₁ : N₁ ⊔ span R t₂ = N₁ ⊔ N₂
Tactic: rw [span_union, span_t₁, span_t₂]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
rw : span R t₁ ⊔ span R t₂ = N₁ ⊔ N₂
rw₁ : N₁ ⊔ span R t₂ = N₁ ⊔ N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw₂ : N₁ ⊔ N₂ = N₁ ⊔ N₂
Tactic: rw [span_union, span_t₁, span_t₂]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_3
inst_3 : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
⊢ (iSup N).FG
have intro : ∀ (val : Fintype (PLift ι)), (iSup N).FG
Tactic: cases nonempty_fintype (PLift ι)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
R_1 : Type u_1
M : Type u_2
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
P Q R : { P : Submodule R_1 M // P.FG }
hPR : P ≤ R
hQR : Q ≤ R
⊢ Subtype.mk (p := fun (P : Submodule R_1 M) ↦ P.FG) ((↑P : Submodule R_1 M) ⊔ (↑Q : Submodule R_1 M)) ⋯ ≤ R
have hPR₁ : (↑P : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)
Tactic: rw [← Subtype.coe_le_coe] at hPR hQR ⊢
Cleared hypotheses: hPR, hQR