variable {ι 𝕜 E F : Type*}

open Topology TopologicalSpace
open scoped NNReal

section

section TopologicalRing

variable [Finite ι] [Field 𝕜] [t𝕜 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [T0Space 𝕜]

theorem LinearMap.mem_span_iff_continuous_of_finite {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
    φ ∈ Submodule.span 𝕜 (Set.range f) ↔
    Continuous[⨅ i, induced (f i) t𝕜, t𝕜] φ := by
  let _ := ⨅ i, induced (f i) t𝕜
  constructor
  · exact Submodule.span_induction
      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c)
  · intro φ_cont
    refine mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_
    simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢
    have : Inseparable x 0 := by
      -- Maybe missing lemmas about `Inseparable`?
      simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
    simpa only [map_zero] using (this.map φ_cont).eq

end TopologicalRing

section NontriviallyNormedField

variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]

theorem LinearMap.mem_span_iff_continuous {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
    φ ∈ Submodule.span 𝕜 (Set.range f) ↔
    Continuous[⨅ i, induced (f i) inferInstance, inferInstance] φ := by
  letI t𝕜 : TopologicalSpace 𝕜 := inferInstance
  let t := ⨅ i, induced (f i) t𝕜
  constructor
  -- TODO: is it worth factoring the first implication with `mem_span_iff_continuous_of_finite`?
  · exact Submodule.span_induction
      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c)
  · intro φ_cont
    obtain ⟨s, hs⟩ : ∃ s : Finset ι, Continuous[⨅ i : s, induced (f i) t𝕜, t𝕜] φ := by
      -- The following should be golfable by using/developping better API
      have : φ ⁻¹' (Metric.ball 0 1) ∈ 𝓝 0 :=
        φ_cont.continuousAt.tendsto (map_zero φ ▸ Metric.ball_mem_nhds (0 : 𝕜) one_pos)
      rw [nhds_iInf, Filter.mem_iInf_finite] at this
      rcases this with ⟨s, hs⟩
      use s
      let t' := ⨅ i : s, induced (f i) t𝕜
      have : IsTopologicalAddGroup E :=
        topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
      have : ContinuousSMul 𝕜 E :=
        continuousSMul_iInf fun _ ↦ continuousSMul_induced _
      rw [Seminorm.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const]
      refine Seminorm.continuous (r := 1) ?_
      rwa [nhds_iInf, Seminorm.ball_comp, ball_normSeminorm, iInf_subtype, map_zero]
    rw [← LinearMap.mem_span_iff_continuous_of_finite] at hs
    exact Submodule.span_mono (Set.range_comp_subset_range _ _) hs

theorem LinearMap.mem_span_iff_bound [Nonempty ι] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
    φ ∈ Submodule.span 𝕜 (Set.range f) ↔
    ∃ s : Finset ι, ∃ c : ℝ≥0, (normSeminorm 𝕜 𝕜).comp φ ≤
      c • (s.sup fun i ↦ (normSeminorm 𝕜 𝕜).comp (f i)) := by
  letI t𝕜 : TopologicalSpace 𝕜 := inferInstance
  let t := ⨅ i, induced (f i) t𝕜
  have : IsTopologicalAddGroup E := topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
  have : WithSeminorms (fun i ↦ (normSeminorm 𝕜 𝕜).comp (f i)) := by
    simp_rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_iInf, nhds_induced, map_zero,
      ← comap_norm_nhds_zero (E := 𝕜), Filter.comap_comap]
    rfl
  rw [LinearMap.mem_span_iff_continuous]
  constructor <;> intro H
  · rw [Seminorm.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const] at H
    rcases Seminorm.bound_of_continuous this _ H with ⟨s, C, -, hC⟩
    exact ⟨s, C, hC⟩
  · exact Seminorm.cont_withSeminorms_normedSpace _ this _ H

end NontriviallyNormedField

end