-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
simp :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
      Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
simp₁ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    closure[Pi.topologicalSpace]
        (Set.pi (α := E) univ fun (i : ι) ↦ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i))) ⊆
      closure[Pi.topologicalSpace]
        (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
simp₂ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    closure[Pi.topologicalSpace]
        (↑(⨆ (i : ι),
              Submodule.span 𝕜
                ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
                  tangentConeAt 𝕜 (s i) (x i))) :
          Set ((i : ι) → E i)) ⊆
      closure[Pi.topologicalSpace]
        (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
h₁ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    LE.le (α := Submodule 𝕜 ((i : ι) → E i))
      (⨆ (i : ι),
        Submodule.span 𝕜
          ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
            tangentConeAt 𝕜 (s i) (x i)))
      (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
h₂ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i))
    (i : ι),
    LE.le (α := Submodule 𝕜 ((i : ι) → E i))
      (Submodule.span 𝕜
        ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
          tangentConeAt 𝕜 (s i) (x i)))
      (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
h₃ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i))
    (i : ι),
    (⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) '' tangentConeAt 𝕜 (s i) (x i) ⊆
      tangentConeAt 𝕜 (Set.pi (α := E) univ s) x
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x

Tactic:
classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
  simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]
  gcongr
  refine iSup_le fun i ↦ ?_
  gcongr
  exact mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset

Premises used: uniqueDiffWithinAt_iff, Submodule.closure_coe_iSup_map_single, closure_pi_set, iSup_le, Submodule.map_span