awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
S : Submodule R M
⊢ S.CoFG

Tactic:
Module.Finite.quotient R S

Premises used: Module.Finite.quotient
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ CoFG.{u_1, u_2} (R := R) (M := M) ⊤

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ CoFG.{u_1, u_2} (R := R) (M := M) ⊥ ↔ Module.Finite R M

Tactic:
⟨fun _ => Module.Finite.equiv (quotEquivOfEqBot ⊥ rfl), fun _ => CoFG.of_finite⟩

Premises used: Submodule.quotEquivOfEqBot, Bot.bot, Submodule.CoFG.of_finite, Iff.intro, Module.Finite.equiv, rfl
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : IsCompl S T
hS : S.CoFG
⊢ T.FG

Tactic:
Module.Finite.iff_fg.mp <| Module.Finite.equiv <| quotientEquivOfIsCompl S T hST

Premises used: Submodule.quotientEquivOfIsCompl, Iff.mp, Module.Finite.iff_fg, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : IsCompl S T
hS : S.FG
⊢ Module.Finite.{u_1, u_2} R ↥S

Tactic:
haveI := Module.Finite.iff_fg.mpr hS
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : IsCompl S T
hS : S.FG
this : Module.Finite.{u_1, u_2} R ↥S
⊢ T.CoFG

Tactic:
Module.Finite.equiv (quotientEquivOfIsCompl T S hST.symm).symm

Premises used: LinearEquiv.symm, Submodule.quotientEquivOfIsCompl, Module.Finite.equiv, IsCompl.symm
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : IsCompl S T
hS : S.FG
this : Module.Finite.{u_1, u_2} R ↥S
⊢ T.CoFG

Tactic:
exact Module.Finite.equiv (quotientEquivOfIsCompl T S hST.symm).symm

Premises used: LinearEquiv.symm, Submodule.quotientEquivOfIsCompl, Module.Finite.equiv, IsCompl.symm
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hT : S ≤ T
hS : S.CoFG
rw : (S ⊔ T).CoFG
⊢ T.CoFG

Tactic:
rw [← sup_eq_right.mpr hT]

Premises used: Iff.mpr, sup_eq_right
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hT : S ≤ T
hS : S.CoFG
⊢ (S ⊔ T).CoFG

Tactic:
Module.Finite.equiv (quotientQuotientEquivQuotientSup S T)

Premises used: Submodule.quotientQuotientEquivQuotientSup, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hT : S ≤ T
hS : S.CoFG
⊢ (S ⊔ T).CoFG

Tactic:
exact Module.Finite.equiv (quotientQuotientEquivQuotientSup S T)

Premises used: Submodule.quotientQuotientEquivQuotientSup, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
rw : Module.Finite.{u_1, u_3} R ↥f.range ↔ f.ker.CoFG
⊢ f.range.FG ↔ f.ker.CoFG

Tactic:
rw [← Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ Module.Finite.{u_1, u_3} R ↥f.range ↔ f.ker.CoFG

Tactic:
Module.Finite.equiv_iff <| f.quotKerEquivRange.symm

Premises used: LinearEquiv.symm, Module.Finite.equiv_iff, LinearMap.quotKerEquivRange
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ Module.Finite.{u_1, u_3} R ↥f.range ↔ f.ker.CoFG

Tactic:
exact Module.Finite.equiv_iff <| f.quotKerEquivRange.symm

Premises used: LinearEquiv.symm, Module.Finite.equiv_iff, LinearMap.quotKerEquivRange
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R N
f : M →ₗ[R] N
⊢ f.ker.CoFG

Tactic:
range_fg_iff_ker_cofg.mp <| IsNoetherian.noetherian _

Premises used: Submodule.range_fg_iff_ker_cofg, IsNoetherian.noetherian, Iff.mp
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
rw : (S.mkQ.prod T.mkQ).ker.CoFG
⊢ (S ⊓ T).CoFG

Tactic:
rw [← Submodule.ker_mkQ S, ← Submodule.ker_mkQ T, ← LinearMap.ker_prod]

Premises used: LinearMap.ker_prod, Submodule.ker_mkQ
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S.mkQ.prod T.mkQ).ker.CoFG

Tactic:
CoFG.ker _

Premises used: Submodule.CoFG.ker
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S.mkQ.prod T.mkQ).ker.CoFG

Tactic:
exact CoFG.ker _

Premises used: Submodule.CoFG.ker
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
hs : ∀ (S : Submodule R M), Membership.mem (γ := Finset (Submodule R M)) ∅ S → S.CoFG
⊢ (sInf (↑∅ : Set (Submodule R M))).CoFG

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
w : Submodule R M
s : Finset (Submodule R M)
hws : w ∉ s
hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG
hs : ∀ S ∈ Insert.insert w s, S.CoFG
insert : ∀ (hs : w.CoFG ∧ ∀ a ∈ s, a.CoFG), (w ⊓ sInf (↑s : Set (Submodule R M))).CoFG
⊢ (sInf (↑(Insert.insert w s) : Set (Submodule R M))).CoFG

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *

Premises used: Finset.mem_insert, forall_eq_or_imp, sInf_insert, Finset.coe_insert
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
w : Submodule R M
s : Finset (Submodule R M)
hws : w ∉ s
hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG
hs : w.CoFG ∧ ∀ a ∈ s, a.CoFG
⊢ (w ⊓ sInf (↑s : Set (Submodule R M))).CoFG

Tactic:
hs.1.inf (hs' hs.2)

Premises used: And.right, And.left, Submodule.CoFG.inf
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
w : Submodule R M
s : Finset (Submodule R M)
hws : w ∉ s
hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG
hs : w.CoFG ∧ ∀ a ∈ s, a.CoFG
⊢ (w ⊓ sInf (↑s : Set (Submodule R M))).CoFG

Tactic:
exact hs.1.inf (hs' hs.2)

Premises used: And.right, And.left, Submodule.CoFG.inf
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset (Submodule R M)
hs : ∀ S ∈ s, S.CoFG
empty :
  ∀ (hs : ∀ (S : Submodule R M), Membership.mem (γ := Finset (Submodule R M)) ∅ S → S.CoFG),
    (sInf (↑∅ : Set (Submodule R M))).CoFG
insert :
  ∀ (w : Submodule R M) (s : Finset (Submodule R M)) (hws : w ∉ s)
    (hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG) (hs : ∀ S ∈ Insert.insert w s, S.CoFG),
    (sInf (↑(Insert.insert w s) : Set (Submodule R M))).CoFG
⊢ (sInf (↑s : Set (Submodule R M))).CoFG

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert w s hws hs' =>
    simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *
    exact hs.1.inf (hs' hs.2)

Premises used: Insert.insert, Finset.mem_insert, forall_eq_or_imp, sInf_insert, Finset.coe_insert
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset (Submodule R M)
hs : ∀ S ∈ s, S.CoFG
empty :
  ∀ (hs : ∀ (S : Submodule R M), Membership.mem (γ := Finset (Submodule R M)) ∅ S → S.CoFG),
    (sInf (↑∅ : Set (Submodule R M))).CoFG
insert :
  ∀ (w : Submodule R M) (s : Finset (Submodule R M)) (hws : w ∉ s)
    (hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG) (hs : ∀ S ∈ Insert.insert w s, S.CoFG),
    (sInf (↑(Insert.insert w s) : Set (Submodule R M))).CoFG
⊢ (sInf (↑s : Set (Submodule R M))).CoFG

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert w s hws hs' =>
    simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *
    exact hs.1.inf (hs' hs.2)

Premises used: Insert.insert, Finset.mem_insert, forall_eq_or_imp, sInf_insert, Finset.coe_insert
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Set (Submodule R M)
hs : s.Finite
hcofg : ∀ S ∈ s, S.CoFG
rw :
  ∀ (hcofg : ∀ S ∈ (↑(hs.toFinset (s := s)) : Set (Submodule R M)), S.CoFG),
    (sInf (↑(hs.toFinset (s := s)) : Set (Submodule R M))).CoFG
⊢ (sInf s).CoFG

Tactic:
rw [← hs.coe_toFinset] at hcofg ⊢

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Set (Submodule R M)
hs : s.Finite
hcofg : ∀ S ∈ (↑(hs.toFinset (s := s)) : Set (Submodule R M)), S.CoFG
⊢ (sInf (↑(hs.toFinset (s := s)) : Set (Submodule R M))).CoFG

Tactic:
CoFG.sInf hcofg

Premises used: Submodule.CoFG.sInf
-- Module: Mathlib.RingTheory.Finiteness.Cofinite
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Set (Submodule R M)
hs : s.Finite
hcofg : ∀ S ∈ (↑(hs.toFinset (s := s)) : Set (Submodule R M)), S.CoFG
⊢ (sInf (↑(hs.toFinset (s := s)) : Set (Submodule R M))).CoFG

Tactic:
exact CoFG.sInf hcofg

Premises used: Submodule.CoFG.sInf
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
⊢ N.FG ↔ ∃ (S : Set M), S.Finite ∧ span R S = N

Tactic:
⟨fun ⟨t, h⟩ => ⟨_, t.finite_toSet, h⟩, ?_⟩

Premises used: Set.Finite, _private.0.Submodule.fg_def.match_1, Exists, And, SetLike.coe, And.intro, Iff.intro, Exists.intro, Submodule.span, Finset.finite_toSet, Eq
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
refine : (∃ (S : Set M), S.Finite ∧ span R S = N) → N.FG
⊢ N.FG ↔ ∃ (S : Set M), S.Finite ∧ span R S = N

Tactic:
refine ⟨fun ⟨t, h⟩ => ⟨_, t.finite_toSet, h⟩, ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
t' : Set M
h : t'.Finite
⊢ ∃ (s' : Finset M), (↑s' : Set M) = t'

Tactic:
have := h.exists_finset_coe
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
t' : Set M
h : t'.Finite
this : ∃ (s' : Finset M), (↑s' : Set M) = t'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (w : Finset M), (↑w : Set M) = t' → FG (span R t')
⊢ FG (span R t')

Tactic:
tauto
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
M : Type u_2
inst : AddCommMonoid M
P : Submodule ℕ M
h : P.FG
S : Finset M
hS : span ℕ (↑S : Set M) = P
⊢ AddSubmonoid.closure (↑S : Set M) = P.toAddSubmonoid

Tactic:
simpa [← span_nat_eq_addSubmonoidClosure]

Premises used: Submodule.span_nat_eq_addSubmonoidClosure
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
M : Type u_2
inst : AddCommMonoid M
P : Submodule ℕ M
h : P.FG
S : Finset M
hS : AddSubmonoid.closure (↑S : Set M) = P.toAddSubmonoid
⊢ span ℕ (↑S : Set M) = P

Tactic:
simpa [← span_nat_eq_addSubmonoidClosure] using hS

Premises used: Submodule.span_nat_eq_addSubmonoidClosure
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
G : Type u_3
inst : AddCommGroup G
P : Submodule ℤ G
h : P.FG
S : Finset G
hS : span ℤ (↑S : Set G) = P
⊢ AddSubgroup.closure (↑S : Set G) = P.toAddSubgroup

Tactic:
simpa [← span_int_eq_addSubgroupClosure]

Premises used: Submodule.span_int_eq_addSubgroupClosure
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
G : Type u_3
inst : AddCommGroup G
P : Submodule ℤ G
h : P.toAddSubgroup.FG
S : Finset G
hS : AddSubgroup.closure (↑S : Set G) = P.toAddSubgroup
⊢ span ℤ (↑S : Set G) = P

Tactic:
simpa [← span_int_eq_addSubgroupClosure] using hS

Premises used: Submodule.span_int_eq_addSubgroupClosure
-- Module: Mathlib.RingTheory.Finiteness.Defs
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 : (∃ (S : Set M), S.Finite ∧ span R S = N) ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
⊢ N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N

Tactic:
rw [fg_def]

Premises used: Submodule.fg_def
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
mp : (∃ (S : Set M), S.Finite ∧ span R S = N) → ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
mpr : (∃ (n : ℕ) (s : Fin n → M), span R (range s) = N) → ∃ (S : Set M), S.Finite ∧ span R S = N
⊢ (∃ (S : Set M), S.Finite ∧ span R S = N) ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N

Tactic:
constructor
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
S : Set M
Sfin : S.Finite
hS : span R S = N
mp :
  ∀ (n : ℕ) (f : Fin n ↪ M) (Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M)))
    (hS : span R (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N), ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N
⊢ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N

Tactic:
obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding

Premises used: Set.Finite.fin_embedding, rfl
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
n : ℕ
f : Fin n ↪ M
Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M))
hS : span R (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N
⊢ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N

Tactic:
⟨n, f, hS⟩

Premises used: Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
n : ℕ
f : Fin n ↪ M
Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M))
hS : span R (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N
⊢ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N

Tactic:
exact ⟨n, f, hS⟩
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
n : ℕ
s : Fin n → M
hs : span R (range s) = N
⊢ ∃ (S : Set M), S.Finite ∧ span R S = N

Tactic:
⟨range s, finite_range s, hs⟩

Premises used: Set.finite_range, And.intro, Exists.intro, Set.range
-- Module: Mathlib.RingTheory.Finiteness.Defs
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
n : ℕ
s : Fin n → M
hs : span R (range s) = N
⊢ ∃ (S : Set M), S.Finite ∧ span R S = N

Tactic:
exact ⟨range s, finite_range s, hs⟩
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
mp : N.FG → ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
mpr : (∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N) → N.FG
⊢ N.FG ↔ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N

Tactic:
constructor
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
mp :
  ∀ (n : ℕ) (f : Fin n → M) (h : span A (range f) = N), ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N
⊢ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N

Tactic:
obtain ⟨n, f, h⟩ := fg_iff_exists_fin_generating_family.mp hN

Premises used: Submodule.fg_iff_exists_fin_generating_family, Iff.mp
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N

Tactic:
⟨ULift (Fin n), inferInstance, f ∘ ULift.down, ?_⟩

Premises used: ULift, Function.comp, inferInstance, Exists.intro, Fin, ULift.down
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
mp : span A (range (f ∘ ULift.down)) = N
⊢ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (range g) = N

Tactic:
refine ⟨ULift (Fin n), inferInstance, f ∘ ULift.down, ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ span A (range f) = N

Tactic:
h
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
h₁ : range (f ∘ ULift.down) = range f
⊢ span A (range (f ∘ ULift.down)) = N

Tactic:
convert! h
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
h₁ : ∀ (x : M), x ∈ range (f ∘ ULift.down) ↔ x ∈ range f
⊢ range (f ∘ ULift.down) = range f

Tactic:
ext
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
x : M
⊢ x ∈ range (f ∘ ULift.down) ↔ x ∈ range f

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
G : Type w
w : Finite G
g : G → M
hg : span A (range g) = N
mpr : ∀ (this : Fintype (↑(range g) : Type v)), N.FG
⊢ N.FG

Tactic:
have := Fintype.ofFinite (range g)
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
G : Type w
w : Finite G
g : G → M
hg : span A (range g) = N
this : Fintype (↑(range g) : Type v)
⊢ span A (↑(range g).toFinset : Set M) = N

Tactic:
simpa
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
A : Type u
inst : Semiring A
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module A M
N : Submodule A M
G : Type w
w : Finite G
g : G → M
hg : span A (range g) = N
this : Fintype (↑(range g) : Type v)
⊢ N.FG

Tactic:
exact ⟨(range g).toFinset, by simpa⟩
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
mp : FG (span R s) → ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
mpr : (∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))) → FG (span R s)
⊢ FG (span R s) ↔ ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))

Tactic:
constructor
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
mp :
  ∀ (s' : Finset M) (hs's : (↑s' : Set M) ⊆ s) (hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)),
    ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
⊢ ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))

Tactic:
obtain ⟨s', hs's, hss'⟩ := subset_span_finite_of_subset_span <| hs'' ▸ subset_span

Premises used: Submodule.subset_span_finite_of_subset_span
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
s' : Finset M
hs's : (↑s' : Set M) ⊆ s
hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
⊢ ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))

Tactic:
⟨s', hs's, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
s' : Finset M
hs's : (↑s' : Set M) ⊆ s
hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
mp : Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))
⊢ ∃ (s' : Finset M), (↑s' : Set M) ⊆ s ∧ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))

Tactic:
refine ⟨s', hs's, ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
s' : Finset M
hs's : (↑s' : Set M) ⊆ s
hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
mp : LE.le (α := Submodule R M) (span R s) (span R (↑s' : Set M))
mp₁ : LE.le (α := Submodule R M) (span R (↑s' : Set M)) (span R s)
⊢ Eq (α := Submodule R M) (span R s) (span R (↑s' : Set M))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
s' : Finset M
hs's : (↑s' : Set M) ⊆ s
hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
mp : LE.le (α := Submodule R M) (span R (↑s'' : Set M)) (span R (↑s' : Set M))
mp₁ mp₂ mp₃ mp₄ : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
⊢ LE.le (α := Submodule R M) (span R s) (span R (↑s' : Set M))

Tactic:
rwa [← hs'', span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.RingTheory.Finiteness.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s'' : Finset M
hs'' : Eq (α := Submodule R M) (span R (↑s'' : Set M)) (span R s)
s' : Finset M
hs's : (↑s' : Set M) ⊆ s
hss' : (↑s'' : Set M) ⊆ (↑(span R (↑s' : Set M)) : Set M)
mp : (↑s' : Set M) ⊆ (↑(span R s) : Set M)
⊢ LE.le (α := Submodule R M) (span R (↑s' : Set M)) (span R s)

Tactic:
rw [span_le]

Premises used: Submodule.span_le