awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ↥M'
x_4 x : M
hx : x ∈ Set.range mj
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)
⊢ 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:
obtain ⟨j, rfl⟩ := hx

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 : ↥M'
x : M
j : Fin k
⊢ nj j ∈ {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 : ↥M'
x : M
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:
exact ⟨⟨nj j, subset_span (by simp)⟩, hnj j⟩
-- 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 : ↥M'
x : M
⊢ 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'))
    0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_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 : ↥M'
x : M
⊢ 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'))
    0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_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 : ↥M'
x_4 : M
a : ↥A
x : M
hx_1 : Membership.mem (γ := Submodule (↥A) M) (span (↥A) (Set.range mj)) x
hx :
  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
⊢ 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'))
    (a • x)

Tactic:
smul_mem _ a hx

Premises used: 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_3 : ↥M'
x_4 : M
a : ↥A
x : M
hx_1 : Membership.mem (γ := Submodule (↥A) M) (span (↥A) (Set.range mj)) x
hx :
  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
⊢ 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'))
    (a • x)

Tactic:
exact smul_mem _ a hx

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.Finiteness.Basic
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 ∅) ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊥
⊢ Eq (α := Submodule R M) (span R (↑∅ : Set M)) ⊥

Tactic:
rw [Finset.coe_empty, span_empty]

Premises used: Finset.coe_empty, Submodule.span_empty
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
rw rw₁ : Eq (α := Submodule R M) (span R s) (span R s)
⊢ Eq (α := Submodule R M) (span R (↑(hs.toFinset (s := s)) : Set M)) (span R s)

Tactic:
rw [hs.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ FG (M := M) (R ∙ x)

Tactic:
fg_span (finite_singleton x)

Premises used: Set.finite_singleton, Submodule.fg_span
-- Module: Mathlib.RingTheory.Finiteness.Basic
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₂
rw₂ rw₃ : N₁ ⊔ N₂ = N₁ ⊔ N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [span_union, span_t₁, span_t₂]

Premises used: Submodule.span_union
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
s : Finset ι
N : ι → Submodule R M
h : ∀ i ∈ s, (N i).FG
⊢ (s.sup N).FG

Tactic:
Finset.sup_induction fg_bot (fun _ ha _ hb => ha.sup hb) h

Premises used: Finset.sup_induction, Submodule.FG.sup, Submodule.fg_bot
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
s : Finset ι
N : ι → Submodule R M
h : ∀ i ∈ s, (N i).FG
⊢ FG.{u_1, u_2} (R := R) (M := M) (⨆ i ∈ s, N i)

Tactic:
simpa only [Finset.sup_eq_iSup] using fg_finset_sup s N h

Premises used: Submodule.fg_finset_sup, Finset.sup_eq_iSup
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
intro : ∀ (val : Fintype (PLift ι)), (iSup N).FG
⊢ (iSup N).FG

Tactic:
cases nonempty_fintype (PLift ι)

Premises used: PLift, nonempty_fintype
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
val : Fintype (PLift ι)
⊢ (iSup N).FG

Tactic:
simpa [iSup_plift_down] using fg_biSup Finset.univ (N ∘ PLift.down) fun i _ => h i.down

Premises used: Finset.univ, Submodule.fg_biSup, iSup_plift_down, Function.comp, PLift.down
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // P.FG }
⊢ (↑P : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
le_sup_left

Premises used: le_sup_left, Set.Mem
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // P.FG }
⊢ (↑P : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // P.FG }
⊢ (↑Q : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
le_sup_right

Premises used: Set.Mem, le_sup_right
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : { P : Submodule R M // P.FG }
⊢ (↑Q : Submodule R M) ≤
    (↑(Subtype.mk (p := fun (P : Submodule R M) ↦ P.FG) ((↑P : Submodule R M) ⊔ (↑Q : Submodule R M)) ⋯) :
      Submodule R M)

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
⊢ (↑P : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)

Tactic:
rw [← Subtype.coe_le_coe] at hPR hQR ⊢

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
hPR₁ : (↑P : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)
⊢ (↑Q : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)

Tactic:
rw [← Subtype.coe_le_coe] at hPR hQR ⊢

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.RingTheory.Finiteness.Basic
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 : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)
hQR : (↑Q : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)
⊢ (↑(Subtype.mk (p := fun (P : Submodule R_1 M) ↦ P.FG) ((↑P : Submodule R_1 M) ⊔ (↑Q : Submodule R_1 M)) ⋯) :
      Submodule R_1 M) ≤
    (↑R : Submodule R_1 M)

Tactic:
sup_le hPR hQR

Premises used: Set.Mem, sup_le
-- Module: Mathlib.RingTheory.Finiteness.Basic
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 : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)
hQR : (↑Q : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)
⊢ (↑(Subtype.mk (p := fun (P : Submodule R_1 M) ↦ P.FG) ((↑P : Submodule R_1 M) ⊔ (↑Q : Submodule R_1 M)) ⋯) :
      Submodule R_1 M) ≤
    (↑R : Submodule R_1 M)

Tactic:
exact sup_le hPR hQR

Premises used: sup_le
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_5
M : ι → Type u_6
inst_1 : Finite ι
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), (p i).FG
simp_rw :
  ∀ (hsb : ∀ (i : ι), ∃ (S : Set (M i)), S.Finite ∧ span R S = p i),
    ∃ (S : Set ((i : ι) → M i)), S.Finite ∧ span R S = pi (φ := M) univ p
⊢ (pi (φ := M) univ p).FG

Tactic:
simp_rw [fg_def] at hsb ⊢

Premises used: Submodule.fg_def