awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι), ∃ (S : Set (M i)), S.Finite ∧ span R S = p i
choose :
  ∀ (t : (i : ι) → Set (M i)) (htf : ∀ (i : ι), (t i).Finite) (hts : ∀ (i : ι), span R (t i) = p i),
    ∃ (S : Set ((i : ι) → M i)), S.Finite ∧ span R S = pi (φ := M) univ p
⊢ ∃ (S : Set ((i : ι) → M i)), S.Finite ∧ span R S = pi (φ := M) univ p

Tactic:
choose t htf hts using hsb
-- 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)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ∃ (S : Set ((i : ι) → M i)), S.Finite ∧ span R S = pi (φ := M) univ p

Tactic:
⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩

Premises used: Set.finite_iUnion, LinearMap.single, Set.Finite.image, And.intro, Exists.intro, Set.image, DFunLike.coe, Set.iUnion
-- 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)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
R₁ : span R (⋃ (i : ι), (⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p
⊢ ∃ (S : Set ((i : ι) → M i)), S.Finite ∧ span R S = pi (φ := M) univ p

Tactic:
refine
      ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
-- 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)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
simp_rw : ⨆ (i : ι), span R ((⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p
simp_rw₁ : ⨆ (i : ι), map (LinearMap.single R M i) (span R (t i)) = pi (φ := M) univ p
simp_rw₂ : ⨆ (i : ι), map (LinearMap.single R M i) (p i) = pi (φ := M) univ p
⊢ span R (⋃ (i : ι), (⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p

Tactic:
simp_rw [span_iUnion, span_image _, hts, iSup_map_single]

Premises used: Submodule.span_iUnion, Submodule.iSup_map_single, Submodule.span_image
-- 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
simp_rw₁ :
  ∀ (t : (i : ι) → Set (M i)) (htf : ∀ (i : ι), (t i).Finite) (hts : ∀ (i : ι), span R (t i) = p i),
    ∃ (S : Set ((i : ι) → M i)), S.Finite ∧ span R S = pi (φ := M) univ p
simp_rw₂ :
  ∀ (t : (i : ι) → Set (M i)) (htf : ∀ (i : ι), (t i).Finite) (hts : ∀ (i : ι), span R (t i) = p i),
    span R (⋃ (i : ι), (⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p
⊢ (pi (φ := M) univ p).FG

Tactic:
classical
    simp_rw [fg_def] at hsb ⊢
    choose t htf hts using hsb
    refine
      ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `span_image` into `span_image _`
    simp_rw [span_iUnion, span_image _, hts, iSup_map_single]

Premises used: Submodule.fg_def, Submodule.span_iUnion, Submodule.iSup_map_single, Submodule.span_image
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
N : Submodule R M
hs : N.FG
t : Set M
ht : t.Finite
span_t : span R t = N
rw : Submodule.map f (span R t) = Submodule.map f N
rw₁ rw₂ : Submodule.map f N = Submodule.map f N
⊢ span S ((⇑f : (a : M) → P) '' t) = Submodule.map f N

Tactic:
rw [span_image, span_t]

Premises used: Submodule.span_image
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
inst_7 : Module.Finite R M
f : M →ₛₗ[σ] P
rw : (map f ⊤).FG
⊢ f.range.FG

Tactic:
rw [LinearMap.range_eq_map]

Premises used: LinearMap.range_eq_map
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
inst_7 : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ (map f ⊤).FG

Tactic:
Module.Finite.fg_top.map f

Premises used: Module.Finite.fg_top, Submodule.FG.map
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
inst_7 : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ (map f ⊤).FG

Tactic:
exact Module.Finite.fg_top.map f

Premises used: Module.Finite.fg_top, Submodule.FG.map
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S (↑t : Set P) = map f N
rw : (↑t : Set P) ⊆ range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → P)
⊢ map f (span R (↑(t.preimage (⇑f : (a : M) → P) ⋯) : Set M)) = map f N

Tactic:
rw [map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
        Set.inter_eq_self_of_subset_left, ht]

Premises used: Set.image_preimage_eq_inter_range, Finset.coe_preimage, Submodule.map_span, Set.inter_eq_self_of_subset_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
S : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S (↑t : Set P) = map f N
rw : map f N ≤ map f ⊤
⊢ (↑t : Set P) ⊆ range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → P)

Tactic:
rw [← LinearMap.coe_range, ← span_le, ht, ← map_top]

Premises used: Submodule.map_top, LinearMap.coe_range, Submodule.span_le
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S (↑t : Set P) = map f N
⊢ map f N ≤ map f ⊤

Tactic:
map_mono le_top

Premises used: le_top, Submodule.map_mono
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S (↑t : Set P) = map f N
⊢ map f N ≤ map f ⊤

Tactic:
exact map_mono le_top

Premises used: le_top, Submodule.map_mono
-- 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 : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
N : Submodule R M
⊢ (map f N).FG ↔ N.FG

Tactic:
⟨(fg_of_fg_map_injective _ hf ·), (.map _)⟩

Premises used: Submodule.FG.map, Iff.intro, Submodule.fg_of_fg_map_injective
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
P : Type u_6
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
hf : f.ker = ⊥
N : Submodule R M
hfn : (map f N).FG
⊢ N.FG

Tactic:
fg_of_fg_map_injective f (LinearMap.ker_eq_bot.mp hf) hfn

Premises used: LinearMap.ker_eq_bot, Iff.mp, Submodule.fg_of_fg_map_injective
-- 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 : Submodule R M
rw : (map N.subtype ⊤).FG ↔ N.FG
rw₁ : N.subtype.range.FG ↔ N.FG
rw₂ rw₃ : N.FG ↔ N.FG
⊢ FG.{u_1, u_2} (R := R) (M := ↥N) ⊤ ↔ N.FG

Tactic:
rw [← fg_map_iff N.subtype Subtype.val_injective, map_top, range_subtype]

Premises used: Submodule.fg_map_iff, Subtype.val_injective, Submodule.map_top, Submodule.subtype, Submodule.range_subtype
-- 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 : Type u_3
inst_3 : AddCommMonoid P
inst_4 : Module R P
e : M ≃ₗ[R] P
h : FG.{u_1, u_3} (R := R) (M := P) ⊤
⊢ FG.{u_1, u_2} (R := R) (M := M) ⊤

Tactic:
e.symm.range ▸ map_top (e.symm : P →ₗ[R] M) ▸ h.map _

Premises used: LinearEquiv.symm, Submodule.map_top, Submodule.FG.map, Eq.rec, LinearEquiv.toLinearMap, LinearEquiv.range
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
N : Submodule R M
hN : N.FG
obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) ⋯
⊢ motive N hN

Tactic:
obtain ⟨s, rfl⟩ := hN

Premises used: rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
⊢ motive (span R (↑∅ : Set M)) ⋯

Tactic:
simpa using singleton 0

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R (↑s : Set M)) ⋯
⊢ motive (span R (↑(insert x s) : Set M)) ⋯

Tactic:
simpa [span_insert, sup_comm] using
      sup (span R s) (R ∙ x) _ (fg_span_singleton _) ih (singleton x)

Premises used: SetLike.coe, sup_comm, Submodule.span, Submodule.fg_span_singleton, Submodule.span_insert, Singleton.singleton
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
s : Finset M
empty : motive (span R (↑∅ : Set M)) ⋯
insert :
  ∀ (x : M) (s : Finset M) (hxs : x ∉ s) (ih : motive (span R (↑s : Set M)) ⋯),
    motive (span R (↑(Insert.insert x s) : Set M)) ⋯
⊢ motive (span R (↑s : Set M)) ⋯

Tactic:
induction s using Finset.induction with
  | empty => simpa using singleton 0
  | insert x s hxs ih =>
    simpa [span_insert, sup_comm] using
      sup (span R s) (R ∙ x) _ (fg_span_singleton _) ih (singleton x)

Premises used: Insert.insert, sup_comm, Submodule.span_insert, OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
N : Submodule R M
hN : N.FG
obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) ⋯
⊢ motive N hN

Tactic:
classical
  obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty => simpa using singleton 0
  | insert x s hxs ih =>
    simpa [span_insert, sup_comm] using
      sup (span R s) (R ∙ x) _ (fg_span_singleton _) ih (singleton x)

Premises used: Insert.insert, sup_comm, Submodule.span_insert, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
N : Submodule R M
hN : N.FG
obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) ⋯
⊢ motive N hN

Tactic:
obtain ⟨s, rfl⟩ := hN

Premises used: rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
⊢ motive (span R (↑∅ : Set M)) ⋯

Tactic:
simp [bot]
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R (↑s : Set M)) ⋯
w : Finset M
h : Eq (α := Submodule R M) (span R (↑s : Set M)) (span R (↑s : Set M))
⊢ FG (span R (↑s : Set M))

Tactic:
use s
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R (↑s : Set M)) ⋯
⊢ motive (span R (↑(insert x s) : Set M)) ⋯

Tactic:
simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

Premises used: SetLike.coe, sup_comm, Submodule.span, Submodule.span_insert
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
s : Finset M
empty : motive (span R (↑∅ : Set M)) ⋯
insert :
  ∀ (x : M) (s : Finset M) (hxs : x ∉ s) (ih : motive (span R (↑s : Set M)) ⋯),
    motive (span R (↑(Insert.insert x s) : Set M)) ⋯
⊢ motive (span R (↑s : Set M)) ⋯

Tactic:
induction s using Finset.induction with
  | empty => simp [bot]
  | insert x s hxs ih => simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

Premises used: Insert.insert, sup_comm, Submodule.span_insert
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
N : Submodule R M
hN : N.FG
obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) ⋯
⊢ motive N hN

Tactic:
classical
  obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty => simp [bot]
  | insert x s hxs ih => simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

Premises used: Insert.insert, sup_comm, Submodule.span_insert, rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
inst_3 : CommSemiring R
inst_4 : Algebra R A
inst_5 : Module R M
inst_6 : IsScalarTower R A M
hS : S.FG
h : Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
obtain : ∀ (s : Finset M), FG (restrictScalars R (span A (↑s : Set M)))
⊢ FG (restrictScalars R S)

Tactic:
obtain ⟨s, rfl⟩ := hS

Premises used: rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
inst_3 : CommSemiring R
inst_4 : Algebra R A
inst_5 : Module R M
inst_6 : IsScalarTower R A M
h : Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : Finset M
⊢ FG (restrictScalars R (span A (↑s : Set M)))

Tactic:
⟨s, .symm <| restrictScalars_span R A h _⟩

Premises used: Submodule.FG, Exists.intro, Eq.symm, Submodule.restrictScalars_span
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
inst_3 : CommSemiring R
inst_4 : Algebra R A
inst_5 : Module R M
inst_6 : IsScalarTower R A M
h : Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : Finset M
⊢ FG (restrictScalars R (span A (↑s : Set M)))

Tactic:
exact ⟨s, .symm <| restrictScalars_span R A h _⟩
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
hS : FG (restrictScalars R S)
obtain : ∀ (s : Finset M) (e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)), S.FG
⊢ S.FG

Tactic:
obtain ⟨s, e⟩ := hS
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
s : Finset M
e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)
⊢ S.FG

Tactic:
⟨s, restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩

Premises used: Submodule.FG, le_antisymm, Submodule.restrictScalars_injective, Exists.intro
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
s : Finset M
e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)
refine_1 : LE.le (α := Submodule R M) (restrictScalars R (span A (↑s : Set M))) (restrictScalars R S)
refine_2 : LE.le (α := Submodule R M) (restrictScalars R S) (restrictScalars R (span A (↑s : Set M)))
⊢ S.FG

Tactic:
refine ⟨s, restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
s : Finset M
e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)
⊢ (↑s : Set M) ⊆ (↑(restrictScalars R S) : Set M)

Tactic:
have := span_le.mp e.le
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
s : Finset M
e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)
this : (↑s : Set M) ⊆ (↑(restrictScalars R S) : Set M)
refine_1 : span A (↑s : Set M) ≤ S
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : (↑s : Set M) ⊆ (↑S : Set M)
⊢ LE.le (α := Submodule R M) (restrictScalars R (span A (↑s : Set M))) (restrictScalars R S)

Tactic:
rwa [restrictScalars_le, span_le]

Premises used: Submodule.restrictScalars_le, Submodule.span_le
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
s : Finset M
e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)
refine_2 : LE.le (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R (span A (↑s : Set M)))
⊢ LE.le (α := Submodule R M) (restrictScalars R S) (restrictScalars R (span A (↑s : Set M)))

Tactic:
rw [← e]
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
s : Finset M
e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)
⊢ LE.le (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R (span A (↑s : Set M)))

Tactic:
span_le_restrictScalars ..

Premises used: Submodule.span_le_restrictScalars
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
S : Submodule A M
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
s : Finset M
e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)
⊢ LE.le (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R (span A (↑s : Set M)))

Tactic:
exact span_le_restrictScalars ..

Premises used: Submodule.span_le_restrictScalars
-- 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
M' : Submodule R M
hM' : M'.FG
N : ℕ →o Submodule R M
H : iSup (ι := ℕ) (⇑N : (a : ℕ) → Submodule R M) = M'
obtain : ∀ (S : Finset M) (hS : span R (↑S : Set M) = M'), ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n
⊢ ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n

Tactic:
obtain ⟨S, hS⟩ := hM'
-- 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
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup (ι := ℕ) (⇑N : (a : ℕ) → Submodule R M) = M'
S : Finset M
hS : span R (↑S : Set M) = M'
s : ↥S
⊢ Membership.mem (γ := Submodule R M) (⨆ (k : ℕ), (N : (a : ℕ) → Submodule R M) k) (↑s : M)

Tactic:
simpa [H, ← hS] using subset_span s.prop

Premises used: Subtype.prop, Submodule.subset_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
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup (ι := ℕ) (⇑N : (a : ℕ) → Submodule R M) = M'
S : Finset M
hS : span R (↑S : Set M) = M'
⊢ ∀ (s : ↥S), ∃ (n : ℕ), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) n : Submodule R M) (↑s : M)

Tactic:
have (s : S) : ∃ n, (s : M) ∈ N n :=
    (mem_iSup_of_chain N s).mp (by simpa [H, ← hS] using subset_span s.prop)