-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem UniqueDiffWithinAt.univ_pi (ι : Type*) [Finite ι] (E : ι → Type*)
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i)) (x : ∀ i, E i)
    (h : ∀ i, UniqueDiffWithinAt 𝕜 (s i) (x i)) : UniqueDiffWithinAt 𝕜 (Set.pi univ s) x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ (univ.pi fun i => ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i)))) ⊆
    ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x))

Tactic:
norm_cast

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ (Submodule.pi univ fun i => Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ≤
    Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x)) ∧ x ∈ univ.pi fun i => closure (s i)

Tactic:
refine ⟨(dense_pi univ fun i _ => (h i).1).mono ?_, fun i _ => (h i).2⟩

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ (univ.pi fun i => ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i)))) ⊆
    ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x))

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (univ.pi s) x

Tactic:
simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x)) ∧ x ∈ univ.pi fun i => closure (s i)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ (Submodule.pi univ fun i => Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ≤
    Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x)

Tactic:
simp only [← Submodule.iSup_map_single, iSup_le_iff, LinearMap.map_span, Submodule.span_le,
  ← mapsTo']

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ ∀ (i : ι),
    MapsTo (⇑(LinearMap.single 𝕜 E i)) (tangentConeAt 𝕜 (s i) (x i)) ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x))

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (univ.pi s) x

Tactic:
classical
simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
refine ⟨(dense_pi univ fun i _ => (h i).1).mono ?_, fun i _ => (h i).2⟩
norm_cast
simp only [← Submodule.iSup_map_single, iSup_le_iff, LinearMap.map_span, Submodule.span_le,
  ← mapsTo']
exact fun i => (mapsTo_tangentCone_pi fun j _ => (h j).2).mono Subset.rfl Submodule.subset_span

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure (s i)
⊢ ∀ (i : ι),
    MapsTo (⇑(LinearMap.single 𝕜 E i)) (tangentConeAt 𝕜 (s i) (x i)) ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x))

Tactic:
exact fun i => (mapsTo_tangentCone_pi fun j _ => (h j).2).mono Subset.rfl Submodule.subset_span

Result:
no goals