awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n
have h : M' = (N : (a : ℕ) → Submodule R M) (S.attach.sup f)
Tactic: use S.attach.sup f
-- 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
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)
⊢ M' = (N : (a : ℕ) → Submodule R M) (S.attach.sup f)
have h : M' ≤ (N : (a : ℕ) → Submodule R M) (S.attach.sup f)
Tactic: apply le_antisymm
-- 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
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)
⊢ M' = (N : (a : ℕ) → Submodule R M) (S.attach.sup f)
have h₁ : (N : (a : ℕ) → Submodule R M) (S.attach.sup f) ≤ M'
Tactic: apply le_antisymm
-- 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
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)
⊢ M' ≤ (N : (a : ℕ) → Submodule R M) (S.attach.sup f)
have h : (↑S : Set M) ⊆ (↑((N : (a : ℕ) → Submodule R M) (S.attach.sup f) : Submodule R M) : Set M)
Tactic: rw [← hS, span_le]
-- 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
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)
⊢ (N : (a : ℕ) → Submodule R M) (S.attach.sup f) ≤ M'
have 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)
Tactic: rw [← H]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
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
⊢ s.FG ↔ IsCompactElement s
have supr_rw : ∀ (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
-- 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 : 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)
⊢ s.FG ↔ IsCompactElement s
have mp : s.FG → IsCompactElement s
Tactic: constructor
-- 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 : 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
⊢ s.FG ↔ IsCompactElement s
have mpr : IsCompactElement s → s.FG
Tactic: constructor
-- 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
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
⊢ IsCompactElement (α := Submodule R M) (span R (↑t : Set M))
have mp : IsCompactElement (t.sup sp)
Tactic: rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← t.sup_eq_iSup sp]
-- 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
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
⊢ IsCompactElement (t.sup sp)
have mp : ∀ x ∈ t, IsCompactElement (sp x)
Tactic: apply CompleteLattice.isCompactElement_finsetSup
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
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.FG
have 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
Tactic: rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h
Cleared hypotheses: h
-- 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 : 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))
have rw : s = ⨆ a ∈ sp '' (↑s : Set M), a
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
-- 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 : 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
⊢ s = sSup (sp '' (↑s : Set M))
have rw₁ : s = ⨆ b ∈ (↑s : Set M), sp b
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
-- 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 : 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
⊢ s = sSup (sp '' (↑s : Set M))
have rw₂ : s = span R (↑s : Set M)
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
-- 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 : 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)
⊢ s = sSup (sp '' (↑s : Set M))
have rw₃ : span R (↑s : Set M) = s
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
-- 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 : 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
⊢ s = sSup (sp '' (↑s : Set M))
have rw₄ : s = s
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
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.FG
have sSup' : 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]
-- 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 : 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))
⊢ s.FG
have mpr : ∀ (u : Finset (Submodule R M)) (huspan : (↑u : Set (Submodule R M)) ⊆ sp '' (↑s : Set M)) (husup : s ≤ u.sup id), s.FG
Tactic: obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
-- 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 : 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
have suffices : u.sup id ≤ s
Tactic: suffices u.sup id ≤ s from le_antisymm husup this
-- 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 : 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
⊢ u.sup id ≤ s
have rw : sSup (↑u : Set (Submodule R M)) ≤ sSup (sp '' (↑s : Set M))
Tactic: rw [sSup', Finset.sup_id_eq_sSup]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
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.FG
have ssup : 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
-- 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 : 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
⊢ s.FG
have 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
Tactic: obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
Cleared hypotheses: u, huspan, husup, ssup
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
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
⊢ s.FG
have ssup₁ : 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
Cleared hypotheses: ssup
-- 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 : Submodule R M
Introduce Introduce₁ Introduce₂ : s.FG ↔ IsCompactElement s
⊢ s.FG ↔ IsCompactElement s
have 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
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⟩
-- 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 : 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
⊢ s.FG ↔ IsCompactElement s
have 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
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⟩
-- 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 : 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
⊢ s.FG ↔ IsCompactElement s
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ IsCompactElement.{u_4} (α := Submodule R M) ⊤
have rwa : FG.{u_1, u_4} (R := R) (M := M) ⊤
Tactic: rwa [← fg_iff_compact, ← finite_def]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ Module.Finite R M
have intro : ∀ (val : Fintype M), Module.Finite R M
Tactic: cases nonempty_fintype M
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ Eq (α := Submodule R M) (span R (↑Finset.univ : Set M)) ⊤
have rw : Eq.{u_4 + 1} (α := Submodule R M) (span R univ) ⊤
Tactic: rw [Finset.coe_univ, span_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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) ⊤
⊢ Eq (α := Submodule R M) (span R (↑Finset.univ : Set M)) ⊤
have rw₁ : Eq.{u_4 + 1} (α := Submodule R M) ⊤ ⊤
Tactic: rw [Finset.coe_univ, span_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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)
⊢ FG.{u_7, u_6} (R := S) (M := P) ⊤
have rw : (map f ⊤).FG
Tactic: rw [← LinearMap.range_eq_top.mpr hf, ← Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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 σ
f : M →ₛₗ[σ] P
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
h : Module.Finite S P
⊢ (map f ⊤).FG
have rwa : f.range.FG
Tactic: rwa [Submodule.map_top, LinearMap.range_eq_top.mpr hf.surjective, ← Module.finite_def]