no goals
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), FG (p i)
⊢ FG (pi univ p)
classical
  simp_rw [fg_def] at hsb⊢
  choose t htf hts using hsb
  refine
    ⟨⋃ i, (LinearMap.single i : _ →ₗ[R] _) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
  simp_rw [span_iUnion, span_image, hts, Submodule.iSup_map_single]
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), ∃ S, Set.Finite S ∧ span R S = p i
⊢ ∃ S, Set.Finite S ∧ span R S = pi univ p
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), FG (p i)
⊢ FG (pi univ p)
simp_rw [fg_def] at hsb⊢
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), Set.Finite (t i)
hts : ∀ (i : ι), span R (t i) = p i
⊢ ∃ S, Set.Finite S ∧ span R S = pi univ p
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), ∃ S, Set.Finite S ∧ span R S = p i
⊢ ∃ S, Set.Finite S ∧ span R S = pi univ p
choose t htf hts using hsb
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), Set.Finite (t i)
hts : ∀ (i : ι), span R (t i) = p i
⊢ span R (⋃ (i : ι), ↑(LinearMap.single i) '' t i) = pi univ p
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), Set.Finite (t i)
hts : ∀ (i : ι), span R (t i) = p i
⊢ ∃ S, Set.Finite S ∧ span R S = pi univ p
refine
  ⟨⋃ i, (LinearMap.single i : _ →ₗ[R] _) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
no goals
R : Type u_3
M✝ : Type ?u.206566
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R M✝
P : Type ?u.206602
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
f : M✝ →ₗ[R] P
ι : Type u_1
M : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), Set.Finite (t i)
hts : ∀ (i : ι), span R (t i) = p i
⊢ span R (⋃ (i : ι), ↑(LinearMap.single i) '' t i) = pi univ p
simp_rw [span_iUnion, span_image, hts, Submodule.iSup_map_single]