-- Mathlib/Topology/Algebra/Module/Compact.lean
lemma Submodule.isCompact_of_fg [CompactSpace R] {N : Submodule R M} (hN : N.FG) :
    IsCompact (X := M) N

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
hN : N.FG
⊢ IsCompact ↑N

Tactic:
obtain ⟨s, hs⟩ := hN

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
⊢ IsCompact ↑N

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
⊢ LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N

Tactic:
simp [Finsupp.range_linearCombination, hs]

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ Continuous fun f => ∑ i ∈ s.attach, f i • ↑i

Tactic:
continuity

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
⊢ IsCompact ↑N

Tactic:
have : LinearMap.range (Fintype.linearCombination R R (α := s) Subtype.val) = N := by
  simp [Finsupp.range_linearCombination, hs]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ IsCompact ↑N

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ IsCompact ↑(LinearMap.range ((Fintype.linearCombination R R) Subtype.val))

Tactic:
refine isCompact_range ?_

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ Continuous ⇑((Fintype.linearCombination R R) Subtype.val)

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ IsCompact ↑N

Tactic:
rw [← this]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ IsCompact ↑(LinearMap.range ((Fintype.linearCombination R R) Subtype.val))

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ Continuous ⇑((Fintype.linearCombination R R) Subtype.val)

Tactic:
simp only [Fintype.linearCombination, Finset.univ_eq_attach, smul_eq_mul, LinearMap.coe_mk,
  AddHom.coe_mk]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : LinearMap.range ((Fintype.linearCombination R R) Subtype.val) = N
⊢ Continuous fun f => ∑ i ∈ s.attach, f i • ↑i