awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
this :
  ∀ (s : ↥S), ∃ (n : ℕ), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) n : Submodule R M) (↑s : M)
choose :
  ∀ (f : (s : ↥S) → ℕ)
    (hf :
      ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)),
    ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n
⊢ ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n

Tactic:
choose f hf using this
-- 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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
h : M' = (N : (a : ℕ) → Submodule R M) (S.attach.sup f)
⊢ ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n

Tactic:
use S.attach.sup f

Premises used: Finset.attach, Finset.sup
-- 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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
h : M' ≤ (N : (a : ℕ) → Submodule R M) (S.attach.sup f)
h₁ : (N : (a : ℕ) → Submodule R M) (S.attach.sup f) ≤ M'
⊢ M' = (N : (a : ℕ) → Submodule R M) (S.attach.sup f)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
h : (↑S : Set M) ⊆ (↑((N : (a : ℕ) → Submodule R M) (S.attach.sup f) : Submodule R M) : Set M)
⊢ M' ≤ (N : (a : ℕ) → Submodule R M) (S.attach.sup f)

Tactic:
rw [← hS, span_le]

Premises used: 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
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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
s : M
hs : s ∈ (↑S : Set M)
⊢ s ∈ (↑((N : (a : ℕ) → Submodule R M) (S.attach.sup f) : Submodule R M) : Set M)

Tactic:
N.monotone' (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)

Premises used: Set.Mem, Finset.mem_attach, Subtype.mk, Finset.le_sup, OrderHom.monotone'
-- 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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
s : M
hs : s ∈ (↑S : Set M)
⊢ s ∈ (↑((N : (a : ℕ) → Submodule R M) (S.attach.sup f) : Submodule R M) : Set M)

Tactic:
exact N.monotone' (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)

Premises used: Finset.mem_attach, Subtype.mk, Finset.le_sup, OrderHom.monotone'
-- 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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
h :
  LE.le (α := Submodule R M) ((N : (a : ℕ) → Submodule R M) (S.attach.sup f) : Submodule R M)
    (iSup (ι := ℕ) (⇑N : (a : ℕ) → Submodule R M) : Submodule R M)
⊢ (N : (a : ℕ) → Submodule R M) (S.attach.sup f) ≤ M'

Tactic:
rw [← H]
-- 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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
⊢ LE.le (α := Submodule R M) ((N : (a : ℕ) → Submodule R M) (S.attach.sup f) : Submodule R M)
    (iSup (ι := ℕ) (⇑N : (a : ℕ) → Submodule R M) : Submodule R M)

Tactic:
le_iSup ..

Premises used: Set.Mem, le_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
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'
f : (s : ↥S) → ℕ
hf : ∀ (s : ↥S), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) (f s) : Submodule R M) (↑s : M)
⊢ LE.le (α := Submodule R M) ((N : (a : ℕ) → Submodule R M) (S.attach.sup f) : Submodule R M)
    (iSup (ι := ℕ) (⇑N : (a : ℕ) → Submodule R M) : Submodule R M)

Tactic:
exact le_iSup ..

Premises used: le_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
s : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
t : Finset M
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)

Tactic:
rfl
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
⊢ ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)

Tactic:
have supr_rw : ∀ t : Finset M, ⨆ x ∈ t, sp x = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
mp : s.FG → IsCompactElement s
mpr : IsCompactElement s → s.FG
⊢ s.FG ↔ IsCompactElement s

Tactic:
constructor
-- 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
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
t : Finset M
mp : IsCompactElement (t.sup sp)
⊢ IsCompactElement (α := Submodule R M) (span R (↑t : Set M))

Tactic:
rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← t.sup_eq_iSup sp]

Premises used: Finset.sup_eq_iSup, Submodule.span_eq_iSup_of_singleton_spans
-- 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
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
t : Finset M
mp : ∀ x ∈ t, IsCompactElement (sp x)
⊢ IsCompactElement (t.sup sp)

Tactic:
apply CompleteLattice.isCompactElement_finsetSup

Premises used: CompleteLattice.isCompactElement_finsetSup
-- 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
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
t : Finset M
⊢ ∀ x ∈ t, IsCompactElement (sp x)

Tactic:
fun n _ => singleton_span_isCompactElement n

Premises used: Submodule.singleton_span_isCompactElement
-- 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
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
t : Finset M
⊢ ∀ x ∈ t, IsCompactElement (sp x)

Tactic:
exact fun n _ => singleton_span_isCompactElement n

Premises used: Submodule.singleton_span_isCompactElement
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h : IsCompactElement s
⊢ ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id

Tactic:
rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h

Premises used: CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
rw : s = ⨆ a ∈ sp '' (↑s : Set M), a
rw₁ : s = ⨆ b ∈ (↑s : Set M), sp b
rw₂ : s = span R (↑s : Set M)
rw₃ : span R (↑s : Set M) = s
rw₄ rw₅ : s = s
⊢ s = sSup (sp '' (↑s : Set M))

Tactic:
rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]

Premises used: iSup_image, Submodule.span_eq, eq_comm, sSup_eq_iSup, Submodule.span_eq_iSup_of_singleton_spans
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
⊢ s = sSup (sp '' (↑s : Set M))

Tactic:
have sSup' : s = sSup (sp '' ↑s) := by
        rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
mpr :
  ∀ (u : Finset (Submodule R M)) (huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)) (husup : s ≤ u.sup id), s.FG
⊢ s.FG

Tactic:
obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')

Premises used: SetLike.coe, Set.image, le_of_eq
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
u : Finset (Submodule R M)
huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ u.sup id
suffices : u.sup id ≤ s
⊢ s = u.sup id

Tactic:
suffices u.sup id ≤ s from le_antisymm husup this
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
u : Finset (Submodule R M)
huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ u.sup id
rw : sSup (↑u : Set (Submodule R M)) ≤ sSup (sp '' (↑s : Set M))
⊢ u.sup id ≤ s

Tactic:
rw [sSup', Finset.sup_id_eq_sSup]

Premises used: Finset.sup_id_eq_sSup
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
u : Finset (Submodule R M)
huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ u.sup id
⊢ sSup (↑u : Set (Submodule R M)) ≤ sSup (sp '' (↑s : Set M))

Tactic:
sSup_le_sSup huspan

Premises used: Set.Mem, sSup_le_sSup
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
u : Finset (Submodule R M)
huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ u.sup id
⊢ sSup (↑u : Set (Submodule R M)) ≤ sSup (sp '' (↑s : Set M))

Tactic:
exact sSup_le_sSup huspan

Premises used: sSup_le_sSup
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
u : Finset (Submodule R M)
huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ u.sup id
⊢ s = u.sup id

Tactic:
have ssup : s = u.sup id := by
        suffices u.sup id ≤ s from le_antisymm husup this
        rw [sSup', Finset.sup_id_eq_sSup]
        exact sSup_le_sSup huspan
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
u : Finset (Submodule R M)
huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ u.sup id
ssup : s = u.sup id
mpr :
  ∀ (t : Finset M) (huspan : (↑(Finset.image sp t) : Set (Submodule R M)) ⊆ sp '' (↑s : Set M))
    (husup : s ≤ (Finset.image sp t).sup id) (ssup : s = (Finset.image sp t).sup id), s.FG
⊢ s.FG

Tactic:
obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan

Premises used: Finset.subset_set_image_iff, Iff.mp, rfl
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
t : Finset M
huspan : (↑(Finset.image sp t) : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ (Finset.image sp t).sup id
ssup : s = (Finset.image sp t).sup id
⊢ span R (↑t : Set M) = s

Tactic:
rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw,
        ← span_eq_iSup_of_singleton_spans, eq_comm] at ssup

Premises used: eq_comm, Finset.sup_eq_iSup, Finset.sup_image, Submodule.span_eq_iSup_of_singleton_spans, Function.id_comp
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
t : Finset M
huspan : (↑(Finset.image sp t) : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ (Finset.image sp t).sup id
ssup : span R (↑t : Set M) = s
⊢ s.FG

Tactic:
⟨t, ssup⟩

Premises used: Submodule.FG, Exists.intro
-- 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 : Submodule R M
sp : M → Submodule R M := fun (a : M) ↦ R ∙ a
supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)
h :
  ∀ (s_1 : Set (Submodule R M)),
    s ≤ sSup s_1 → ∃ (t : Finset (Submodule R M)), (↑t : Set (Submodule R M)) ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' (↑s : Set M))
t : Finset M
huspan : (↑(Finset.image sp t) : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)
husup : s ≤ (Finset.image sp t).sup id
ssup : span R (↑t : Set M) = s
⊢ s.FG

Tactic:
exact ⟨t, ssup⟩
-- 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 : Submodule R M
Introduce Introduce₁ Introduce₂ : s.FG ↔ IsCompactElement s
Introduce₃ :
  let sp : M → Submodule R M := fun (a : M) ↦ R ∙ a;
  ∀ (supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)),
    s.FG ↔ IsCompactElement s
mp :
  let sp : M → Submodule R M := fun (a : M) ↦ R ∙ a;
  ∀ (supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)),
    s.FG → IsCompactElement s
mpr mpr₁ :
  let sp : M → Submodule R M := fun (a : M) ↦ R ∙ a;
  ∀ (supr_rw : ∀ (t : Finset M), Eq.{u_2 + 1} (α := Submodule R M) (⨆ x ∈ t, sp x) (⨆ x ∈ (↑t : Set M), sp x)),
    IsCompactElement s → s.FG
⊢ s.FG ↔ IsCompactElement s

Tactic:
classical
    -- Introduce shorthand for span of an element
    let sp : M → Submodule R M := fun a => span R {a}
    -- Trivial rewrite lemma; a small hack since simp (only) & rw can't accomplish this smoothly.
    have supr_rw : ∀ t : Finset M, ⨆ x ∈ t, sp x = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl
    constructor
    · rintro ⟨t, rfl⟩
      rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← t.sup_eq_iSup sp]
      apply CompleteLattice.isCompactElement_finsetSup
      exact fun n _ => singleton_span_isCompactElement n
    · intro h
      rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h
      -- s is the Sup of the spans of its elements.
      have sSup' : s = sSup (sp '' ↑s) := by
        rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
      -- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
      obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
      have ssup : s = u.sup id := by
        suffices u.sup id ≤ s from le_antisymm husup this
        rw [sSup', Finset.sup_id_eq_sSup]
        exact sSup_le_sSup huspan
      obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
      rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw,
        ← span_eq_iSup_of_singleton_spans, eq_comm] at ssup
      exact ⟨t, ssup⟩

Premises used: CompleteLattice.isCompactElement_finsetSup, Submodule.singleton_span_isCompactElement, eq_comm, Finset.sup_eq_iSup, Finset.sup_image, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, rfl, Submodule.span_eq_iSup_of_singleton_spans, Function.id_comp
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
rwa : FG.{u_1, u_4} (R := R) (M := M) ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : Module.Finite R M
⊢ IsCompactElement.{u_4} (α := Submodule R M) ⊤

Tactic:
rwa [← fg_iff_compact, ← finite_def]

Premises used: Module.finite_def, Submodule.fg_iff_compact
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite M
intro : ∀ (val : Fintype M), Module.Finite R M
⊢ Module.Finite R M

Tactic:
cases nonempty_fintype M

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite M
val : Fintype M
rw : Eq.{u_4 + 1} (α := Submodule R M) (span R univ) ⊤
rw₁ rw₂ : Eq.{u_4 + 1} (α := Submodule R M) ⊤ ⊤
⊢ Eq (α := Submodule R M) (span R (↑Finset.univ : Set M)) ⊤

Tactic:
rw [Finset.coe_univ, span_univ]

Premises used: Finset.coe_univ, Submodule.span_univ
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite M
val : Fintype M
⊢ Module.Finite R M

Tactic:
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ, span_univ]⟩⟩
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_7
P : Type u_6
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective.{u_4 + 1, u_6 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
rw : (map f ⊤).FG
⊢ FG.{u_7, u_6} (R := S) (M := P) ⊤

Tactic:
rw [← LinearMap.range_eq_top.mpr hf, ← Submodule.map_top]

Premises used: Iff.mpr, Submodule.map_top, LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_7
P : Type u_6
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective.{u_4 + 1, u_6 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
⊢ (map f ⊤).FG

Tactic:
hM.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_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_7
P : Type u_6
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective.{u_4 + 1, u_6 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
⊢ (map f ⊤).FG

Tactic:
exact hM.fg_top.map f

Premises used: Module.Finite.fg_top, Submodule.FG.map