awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd₁ : Tendsto (β := (j : ι_1) → E j) (fun (n : ι) ↦ Pi.single (M := E) i (d n)) l (𝓝 0)
hds₁ : ∀ᶠ (n : ι) in l, x + Pi.single (M := E) i (d n) ∈ closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)
hcd₁ : Tendsto (fun (n : ι) ↦ c n • Pi.single (M := E) i (d n)) l (𝓝 (Pi.single (M := E) i y))
⊢ Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x

Tactic:
apply mem_tangentConeAt_of_seq l c (fun n ↦ Pi.single i (d n))

Premises used: Pi.single, mem_tangentConeAt_of_seq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd₁ : ∀ (x : ι_1), Tendsto (β := E x) (fun (i_1 : ι) ↦ Pi.single (M := E) i (d i_1) x) l (𝓝 (0 x))
⊢ Tendsto (β := (j : ι_1) → E j) (fun (n : ι) ↦ Pi.single (M := E) i (d n)) l (𝓝 0)

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
j : ι_1
hd₁ :
  ∀ (hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)) ⦃y : E j⦄ (hy : y ∈ tangentConeAt 𝕜 (s j) (x j))
    (d : ι → E j) (hd₀ : Tendsto d l (𝓝 0)) (hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j)
    (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
    Tendsto (β := E j) (fun (i : ι) ↦ Pi.single (M := E) j (d i) j) l (𝓝 (0 j))
hd₂ : ∀ (hj : j ≠ i), Tendsto (β := E j) (fun (i_1 : ι) ↦ Pi.single (M := E) i (d i_1) j) l (𝓝 (0 j))
⊢ Tendsto (β := E j) (fun (i_1 : ι) ↦ Pi.single (M := E) i (d i_1) j) l (𝓝 (0 j))

Tactic:
rcases eq_or_ne j i with rfl | hj

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
j : ι_1
hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)
y : E j
hy : y ∈ tangentConeAt 𝕜 (s j) (x j)
d : ι → E j
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (β := E j) (fun (i : ι) ↦ Pi.single (M := E) j (d i) j) l (𝓝 (0 j))

Tactic:
simp [*, tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
j : ι_1
hj : j ≠ i
⊢ Tendsto (β := E j) (fun (i_1 : ι) ↦ Pi.single (M := E) i (d i_1) j) l (𝓝 (0 j))

Tactic:
simp [*, tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : ι) in l, x + Pi.single (M := E) i (d n) ∈ closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)

Tactic:
hds.mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hds₁ :
  ∀ (n : ι) (hn : x i + d n ∈ s i),
    x + Pi.single (M := E) i (d n) ∈ closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)
⊢ ∀ᶠ (n : ι) in l, x + Pi.single (M := E) i (d n) ∈ closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)

Tactic:
refine hds.mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
hds₁ : ∀ (i_1 : ι_1), (x + Pi.single (M := E) i (d n)) i_1 ∈ closure[inst_3 i_1] (s i_1)
⊢ x + Pi.single (M := E) i (d n) ∈ closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)

Tactic:
rw [closure_pi_set, mem_univ_pi]

Premises used: closure_pi_set, Set.mem_univ_pi
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
j : ι_1
hds₁ :
  ∀ (hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)) ⦃y : E j⦄ (hy : y ∈ tangentConeAt 𝕜 (s j) (x j))
    (d : ι → E j) (hd₀ : Tendsto d l (𝓝 0)) (hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j)
    (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)) (hn : x j + d n ∈ s j),
    (x + Pi.single (M := E) j (d n)) j ∈ closure[inst_3 j] (s j)
hds₂ : ∀ (hj : j ≠ i), (x + Pi.single (M := E) i (d n)) j ∈ closure[inst_3 j] (s j)
⊢ (x + Pi.single (M := E) i (d n)) j ∈ closure[inst_3 j] (s j)

Tactic:
rcases eq_or_ne j i with rfl | hj

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
n : ι
j : ι_1
hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)
y : E j
hy : y ∈ tangentConeAt 𝕜 (s j) (x j)
d : ι → E j
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hn : x j + d n ∈ s j
⊢ (x + Pi.single (M := E) j (d n)) j ∈ closure[inst_3 j] (s j)

Tactic:
simp [*, subset_closure hn]

Premises used: subset_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
j : ι_1
hj : j ≠ i
⊢ (x + Pi.single (M := E) i (d n)) j ∈ closure[inst_3 j] (s j)

Tactic:
simp [*, subset_closure hn]

Premises used: subset_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hcd₁ : ∀ (x : ι_1), Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) x) l (𝓝 (Pi.single (M := E) i y x))
⊢ Tendsto (fun (n : ι) ↦ c n • Pi.single (M := E) i (d n)) l (𝓝 (Pi.single (M := E) i y))

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
j : ι_1
hcd₁ :
  ∀ (hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)) ⦃y : E j⦄ (hy : y ∈ tangentConeAt 𝕜 (s j) (x j))
    (d : ι → E j) (hd₀ : Tendsto d l (𝓝 0)) (hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j)
    (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
    Tendsto (fun (i : ι) ↦ (c i • Pi.single (M := E) j (d i)) j) l (𝓝 (Pi.single (M := E) j y j))
hcd₂ :
  ∀ (hj : j ≠ i), Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) j) l (𝓝 (Pi.single (M := E) i y j))
⊢ Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) j) l (𝓝 (Pi.single (M := E) i y j))

Tactic:
rcases eq_or_ne j i with rfl | hj

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
j : ι_1
hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)
y : E j
hy : y ∈ tangentConeAt 𝕜 (s j) (x j)
d : ι → E j
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun (i : ι) ↦ (c i • Pi.single (M := E) j (d i)) j) l (𝓝 (Pi.single (M := E) j y j))

Tactic:
simp [*, tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
j : ι_1
hj : j ≠ i
⊢ Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) j) l (𝓝 (Pi.single (M := E) i y j))

Tactic:
simp [*, tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- 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
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x

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

Premises used: uniqueDiffWithinAt_iff, closure_pi_set
-- 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 : ι), 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

Tactic:
⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩

Premises used: Set.univ, Dense.of_closure, Dense.mono, dense_pi, And.right, And.left, And.intro, Dense.closure
-- 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 : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
refine :
  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))
⊢ 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

Tactic:
refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
-- 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 : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
simp :
  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))
⊢ 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))

Tactic:
simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]

Premises used: Submodule.closure_coe_iSup_map_single, closure_pi_set, Submodule.map_span
-- 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 : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
h₁ :
  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))
⊢ 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))

Tactic:
gcongr
-- 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 : ι), 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))

Tactic:
iSup_le fun i ↦ ?_

Premises used: Set.Mem, iSup_le
-- 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 : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
h₁ :
  ∀ (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))
⊢ 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))

Tactic:
refine iSup_le fun i ↦ ?_

Premises used: iSup_le
-- 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 : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
i : ι
h₁ :
  (⇑(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
⊢ 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))

Tactic:
gcongr