-- Mathlib/RingTheory/Finiteness/Defs.lean
lemma fg_iff_exists_finite_generating_family {A : Type u} [Semiring A] {M : Type v}
    [AddCommMonoid M] [Module A M] {N : Submodule A M} :
    N.FG ↔ ∃ (G : Type w) (_ : Finite G) (g : G → M), Submodule.span A (Set.range g) = N

Proof state:
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG ↔ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
constructor

Result:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG → ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ (∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N) → N.FG

Proof state:
case mp.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : 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 ∘ ULift.down)) = N

Tactic:
convert h

Result:
case h.e'_2.h.e'_6
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ range (f ∘ ULift.down) = range f

Proof state:
case mp.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

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

Result:
case mp.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : 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 ∘ ULift.down)) = N

Proof state:
case h.e'_2.h.e'_6
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ range (f ∘ ULift.down) = range f

Tactic:
ext x

Result:
case h.e'_2.h.e'_6.h
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : 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

Proof state:
case mpr.intro.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
⊢ N.FG

Tactic:
have := Fintype.ofFinite (range g)

Result:
case mpr.intro.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : 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)
⊢ N.FG

Proof state:
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : 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)
⊢ span A ↑(range g).toFinset = N

Tactic:
simpa using hg

Result:
no goals

Proof state:
case mpr.intro.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : 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)
⊢ N.FG

Tactic:
exact ⟨(range g).toFinset, by simpa using hg⟩

Result:
no goals

Proof state:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG → ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
intro hN

Result:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Proof state:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

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

Result:
case mp.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Proof state:
case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ (∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N) → N.FG

Tactic:
rintro ⟨G, _, g, hg⟩

Result:
case mpr.intro.intro.intro
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
⊢ N.FG

Proof state:
case h.e'_2.h.e'_6.h
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : 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 only [Set.mem_range, Function.comp_apply, ULift.exists]

Result:
no goals