awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
R_1 : Type u_1
M : Type u_2
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
P Q R : { P : Submodule R_1 M // P.FG }
hPR : P ≤ R
hQR : Q ≤ R
hPR₁ : (↑P : 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)) ⋯ ≤ R
have hQR₁ : (↑Q : Submodule R_1 M) ≤ (↑R : Submodule R_1 M)
Tactic: rw [← Subtype.coe_le_coe] at hPR hQR ⊢
Cleared hypotheses: hPR, hQR
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ (pi (φ := M) univ p).FG
have 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
Tactic: simp_rw [fg_def] at hsb ⊢
Cleared hypotheses: hsb
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ ∃ (S : Set ((i : ι) → M i)), S.Finite ∧ span R S = pi (φ := M) univ p
have 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
Tactic: choose t htf hts using hsb
Cleared hypotheses: hsb
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
have R₁ : span R (⋃ (i : ι), (⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p
Tactic: refine
      ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ span R (⋃ (i : ι), (⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p
have simp_rw : ⨆ (i : ι), span R ((⇑(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]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ span R (⋃ (i : ι), (⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p
have simp_rw₁ : ⨆ (i : ι), map (LinearMap.single R M i) (span R (t i)) = pi (φ := M) univ p
Tactic: simp_rw [span_iUnion, span_image _, hts, iSup_map_single]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ span R (⋃ (i : ι), (⇑(LinearMap.single R M i) : (a : M i) → (i : ι) → M i) '' t i) = pi (φ := M) univ p
have simp_rw₂ : ⨆ (i : ι), map (LinearMap.single R M i) (p i) = pi (φ := M) univ p
Tactic: simp_rw [span_iUnion, span_image _, hts, iSup_map_single]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ (pi (φ := M) univ p).FG
have 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
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]
Cleared hypotheses: hsb
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
have 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
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]
Cleared hypotheses: hsb
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ (pi (φ := M) univ p).FG
have 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
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]
Cleared hypotheses: hsb
-- 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 : 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
⊢ span S ((⇑f : (a : M) → P) '' t) = Submodule.map f N
have rw : Submodule.map f (span R t) = Submodule.map f N
Tactic: rw [span_image, span_t]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
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
⊢ span S ((⇑f : (a : M) → P) '' t) = Submodule.map f N
have rw₁ : Submodule.map f N = Submodule.map f N
Tactic: rw [span_image, span_t]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
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
⊢ f.range.FG
have rw : (map f ⊤).FG
Tactic: rw [LinearMap.range_eq_map]
-- 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 : 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 (span R (↑(t.preimage (⇑f : (a : M) → P) ⋯) : Set M)) = map f N
have rw : (↑t : Set P) ⊆ range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → P)
Tactic: rw [map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
        Set.inter_eq_self_of_subset_left, ht]
-- 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 : 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
⊢ (↑t : Set P) ⊆ range.{u_4, u_2 + 1} (ι := M) (⇑f : (a : M) → P)
have rw : map f N ≤ map f ⊤
Tactic: rw [← LinearMap.coe_range, ← span_le, ht, ← map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ FG.{u_1, u_2} (R := R) (M := ↥N) ⊤ ↔ N.FG
have rw : (map N.subtype ⊤).FG ↔ N.FG
Tactic: rw [← fg_map_iff N.subtype Subtype.val_injective, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
rw : (map N.subtype ⊤).FG ↔ N.FG
⊢ FG.{u_1, u_2} (R := R) (M := ↥N) ⊤ ↔ N.FG
have rw₁ : N.subtype.range.FG ↔ N.FG
Tactic: rw [← fg_map_iff N.subtype Subtype.val_injective, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
rw : (map N.subtype ⊤).FG ↔ N.FG
rw₁ : N.subtype.range.FG ↔ N.FG
⊢ FG.{u_1, u_2} (R := R) (M := ↥N) ⊤ ↔ N.FG
have rw₂ : N.FG ↔ N.FG
Tactic: rw [← fg_map_iff N.subtype Subtype.val_injective, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ motive N hN
have obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) sorry
Tactic: obtain ⟨s, rfl⟩ := hN
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ motive (span R (↑s : Set M)) ⋯
have empty : motive (span R (↑∅ : Set M)) sorry
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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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)) ⋯
⊢ motive (span R (↑s : Set M)) ⋯
have insert : ∀ (x : M) (s : Finset M) (hxs : x ∉ s) (ih : motive (span R (↑s : Set M)) sorry), motive (span R (↑(insert x s) : Set M)) sorry
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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ motive N hN
have obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) sorry
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)
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ motive N hN
have obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) sorry
Tactic: obtain ⟨s, rfl⟩ := hN
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ FG (span R (↑s : Set M))
have h : Eq (α := Submodule R M) (span R (↑s : Set M)) (span R (↑s : Set M))
Tactic: use s
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ motive (span R (↑s : Set M)) ⋯
have empty : motive (span R (↑∅ : Set M)) sorry
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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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)) ⋯
⊢ motive (span R (↑s : Set M)) ⋯
have insert : ∀ (x : M) (s : Finset M) (hxs : x ∉ s) (ih : motive (span R (↑s : Set M)) sorry), motive (span R (↑(insert x s) : Set M)) sorry
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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ motive N hN
have obtain : ∀ (s : Finset M), motive (span R (↑s : Set M)) sorry
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
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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)
⊢ FG (restrictScalars R S)
have obtain : ∀ (s : Finset M), FG (restrictScalars R (span A (↑s : Set M)))
Tactic: obtain ⟨s, rfl⟩ := hS
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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)
⊢ S.FG
have obtain : ∀ (s : Finset M) (e : Eq (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R S)), S.FG
Tactic: obtain ⟨s, e⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
have refine_1 : LE.le (α := Submodule R M) (restrictScalars R (span A (↑s : Set M))) (restrictScalars R S)
Tactic: refine ⟨s, restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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)
⊢ S.FG
have refine_2 : LE.le (α := Submodule R M) (restrictScalars R S) (restrictScalars R (span A (↑s : Set M)))
Tactic: refine ⟨s, restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
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) (restrictScalars R (span A (↑s : Set M))) (restrictScalars R S)
have this : (↑s : Set M) ⊆ (↑(restrictScalars R S) : Set M)
Tactic: have := span_le.mp e.le
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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)
⊢ LE.le (α := Submodule R M) (restrictScalars R (span A (↑s : Set M))) (restrictScalars R S)
have refine_1 : span A (↑s : Set M) ≤ S
Tactic: rwa [restrictScalars_le, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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
⊢ LE.le (α := Submodule R M) (restrictScalars R (span A (↑s : Set M))) (restrictScalars R S)
have refine_1₁ : (↑s : Set M) ⊆ (↑S : Set M)
Tactic: rwa [restrictScalars_le, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
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) (restrictScalars R S) (restrictScalars R (span A (↑s : Set M)))
have refine_2 : LE.le (α := Submodule R M) (span R (↑s : Set M)) (restrictScalars R (span A (↑s : Set M)))
Tactic: rw [← e]
-- 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
hM' : M'.FG
N : ℕ →o Submodule R M
H : iSup (ι := ℕ) (⇑N : (a : ℕ) → Submodule R M) = M'
⊢ ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n
have obtain : ∀ (S : Finset M) (hS : span R (↑S : Set M) = M'), ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n
Tactic: obtain ⟨S, hS⟩ := hM'
Cleared hypotheses: hM'
-- 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
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'
⊢ ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n
have this : ∀ (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)
-- 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'
this :
  ∀ (s : ↥S), ∃ (n : ℕ), Membership.mem (γ := Submodule R M) ((N : (a : ℕ) → Submodule R M) n : Submodule R M) (↑s : M)
⊢ ∃ (n : ℕ), M' = (N : (a : ℕ) → Submodule R M) n
have 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
Tactic: choose f hf using this
Cleared hypotheses: this