awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
⊢ (⇑(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

Tactic:
mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset

Premises used: Function.update, Pi.single, dite, And.right, mapsTo_tangentConeAt_pi, Set.MapsTo.image_subset
-- 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 : ι
⊢ (⇑(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

Tactic:
exact mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset

Premises used: And.right, mapsTo_tangentConeAt_pi, Set.MapsTo.image_subset
-- 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)
h : ∀ (i : ι), UniqueDiffOn 𝕜 (s i)
⊢ UniqueDiffOn 𝕜 (Set.pi (α := E) univ s)

Tactic:
fun _x hx ↦ .univ_pi fun i ↦ h i _ <| hx i (mem_univ i)

Premises used: UniqueDiffOn, UniqueDiffWithinAt.univ_pi, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
rw : UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s fun (x : ι) ↦ univ)) x
⊢ UniqueDiffWithinAt 𝕜 (I.pi (α := E) s) x

Tactic:
rw [← Set.univ_pi_piecewise_univ]

Premises used: Set.univ_pi_piecewise_univ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s fun (x : ι) ↦ univ)) x

Tactic:
UniqueDiffWithinAt.univ_pi fun i => ?_

Premises used: UniqueDiffWithinAt.univ_pi
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
refine : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s fun (x : ι) ↦ univ)) x

Tactic:
refine UniqueDiffWithinAt.univ_pi fun i => ?_

Premises used: UniqueDiffWithinAt.univ_pi
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
i : ι
pos : ∀ (hi : i ∈ I), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
neg : ∀ (hi : i ∉ I), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)

Tactic:
by_cases hi : i ∈ I
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
i : ι
hi : i ∈ I
⊢ UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)

Tactic:
simp [*, uniqueDiffWithinAt_univ]

Premises used: uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
i : ι
hi : i ∉ I
⊢ UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)

Tactic:
simp [*, uniqueDiffWithinAt_univ]

Premises used: uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
rw rw₁ rw₂ :
  UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s fun (x : ι) ↦ univ)) x
rw₃ : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (I.pi (α := E) s) x

Tactic:
classical
  rw [← Set.univ_pi_piecewise_univ]
  refine UniqueDiffWithinAt.univ_pi fun i => ?_
  by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]

Premises used: Set.univ_pi_piecewise_univ, uniqueDiffWithinAt_univ, UniqueDiffWithinAt.univ_pi
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : DivisionSemiring 𝕜
ι : 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 : TopologicalSpace 𝕜
inst_4 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_5 : (i : ι) → TopologicalSpace (E i)
inst_6 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
I : Set ι
h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i)
⊢ UniqueDiffOn 𝕜 (I.pi (α := E) s)

Tactic:
fun x hx => UniqueDiffWithinAt.pi fun i hi => h i hi (x i) (hx i hi)

Premises used: UniqueDiffOn, UniqueDiffWithinAt.pi
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
ht : y ∈ closure[inst_8] t
rw :
  (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) '' tangentConeAt 𝕜 s x ⊆
    tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y)
⊢ (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Tactic:
rw [← tangentConeAt_closure (s := s ×ˢ t), closure_prod_eq]

Premises used: tangentConeAt_closure, closure_prod_eq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
ht : y ∈ closure[inst_8] t
z : E
hz : z ∈ tangentConeAt 𝕜 s x
rcases :
  ∀ (ι : Type (max u_1 u_2)) (l : Filter ι) (hl : l.NeBot) (c : ι → 𝕜) (d : ι → E) (hd₀ : Tendsto d l (𝓝 0))
    (hds : ∀ᶠ (n : ι) in l, x + d n ∈ s) (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)),
    Membership.mem (α := E × F) (tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y))
      ((LinearMap.inl 𝕜 E F : (a : E) → E × F) z : E × F)
⊢ Membership.mem (α := E × F) (tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y))
    ((LinearMap.inl 𝕜 E F : (a : E) → E × F) z : E × F)

Tactic:
rcases exists_fun_of_mem_tangentConeAt hz with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
ht : y ∈ closure[inst_8] t
z : E
hz : z ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)
n : ι
hn : x + d n ∈ s
⊢ (x, y) + (fun (n : ι) ↦ ((d n, 0) : E × F)) n ∈ closure[inst_3] s ×ˢ closure[inst_8] t

Tactic:
simp [ht, subset_closure hn]

Premises used: subset_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
ht : y ∈ closure[inst_8] t
z : E
hz : z ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)
refine :
  Tendsto (β := E × F) (fun (n : ι) ↦ HSMul.hSMul (β := E × F) (c n) ((fun (n : ι) ↦ ((d n, 0) : E × F)) n)) l
    (𝓝 ((LinearMap.inl 𝕜 E F : (a : E) → E × F) z) : Filter (E × F))
⊢ Membership.mem (α := E × F) (tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y))
    ((LinearMap.inl 𝕜 E F : (a : E) → E × F) z : E × F)

Tactic:
refine mem_tangentConeAt_of_seq l c (fun n ↦ (d n, 0)) (hd₀.prodMk_nhds tendsto_const_nhds)
    (hds.mono fun n hn ↦ by simp [ht, subset_closure hn]) ?_

Premises used: Prod.mk, Filter.Eventually.mono, mem_tangentConeAt_of_seq, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
ht : y ∈ closure[inst_8] t
z : E
hz : z ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)
⊢ Tendsto (β := E × F) (fun (n : ι) ↦ HSMul.hSMul (β := E × F) (c n) ((fun (n : ι) ↦ ((d n, 0) : E × F)) n)) l
    (𝓝 ((LinearMap.inl 𝕜 E F : (a : E) → E × F) z) : Filter (E × F))

Tactic:
simpa using hcd.prodMk_nhds tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : x ∈ closure[inst_3] s
rw :
  (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) '' tangentConeAt 𝕜 t y ⊆
    tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y)
⊢ (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Tactic:
rw [← tangentConeAt_closure (s := s ×ˢ t), closure_prod_eq]

Premises used: tangentConeAt_closure, closure_prod_eq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : x ∈ closure[inst_3] s
z : F
hz : z ∈ tangentConeAt 𝕜 t y
rcases :
  ∀ (ι : Type (max u_1 u_3)) (l : Filter ι) (hl : l.NeBot) (c : ι → 𝕜) (d : ι → F) (hd₀ : Tendsto d l (𝓝 0))
    (hds : ∀ᶠ (n : ι) in l, y + d n ∈ t) (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)),
    Membership.mem (α := E × F) (tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y))
      ((LinearMap.inr 𝕜 E F : (a : F) → E × F) z : E × F)
⊢ Membership.mem (α := E × F) (tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y))
    ((LinearMap.inr 𝕜 E F : (a : F) → E × F) z : E × F)

Tactic:
rcases exists_fun_of_mem_tangentConeAt hz with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : x ∈ closure[inst_3] s
z : F
hz : z ∈ tangentConeAt 𝕜 t y
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → F
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, y + d n ∈ t
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)
n : ι
hn : y + d n ∈ t
⊢ (x, y) + (fun (n : ι) ↦ ((0, d n) : E × F)) n ∈ closure[inst_3] s ×ˢ closure[inst_8] t

Tactic:
simp [hs, subset_closure hn]

Premises used: subset_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : x ∈ closure[inst_3] s
z : F
hz : z ∈ tangentConeAt 𝕜 t y
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → F
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, y + d n ∈ t
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)
refine :
  Tendsto (β := E × F) (fun (n : ι) ↦ HSMul.hSMul (β := E × F) (c n) ((fun (n : ι) ↦ ((0, d n) : E × F)) n)) l
    (𝓝 ((LinearMap.inr 𝕜 E F : (a : F) → E × F) z) : Filter (E × F))
⊢ Membership.mem (α := E × F) (tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y))
    ((LinearMap.inr 𝕜 E F : (a : F) → E × F) z : E × F)

Tactic:
refine mem_tangentConeAt_of_seq l c (fun n ↦ (0, d n)) (tendsto_const_nhds.prodMk_nhds hd₀)
    (hds.mono fun n hn ↦ by simp [hs, subset_closure hn]) ?_

Premises used: Prod.mk, Filter.Eventually.mono, mem_tangentConeAt_of_seq, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : x ∈ closure[inst_3] s
z : F
hz : z ∈ tangentConeAt 𝕜 t y
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → F
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, y + d n ∈ t
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 z)
⊢ Tendsto (β := E × F) (fun (n : ι) ↦ HSMul.hSMul (β := E × F) (c n) ((fun (n : ι) ↦ ((0, d n) : E × F)) n)) l
    (𝓝 ((LinearMap.inr 𝕜 E F : (a : F) → E × F) z) : Filter (E × F))

Tactic:
simpa using tendsto_const_nhds.prodMk_nhds hcd

Premises used: tendsto_const_nhds, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : UniqueDiffWithinAt 𝕜 s x
ht : UniqueDiffWithinAt 𝕜 t y
rw :
  ∀ (hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s)
    (ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t),
    Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F)) ∧
      (x, y) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)
⊢ UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)

Tactic:
rw [uniqueDiffWithinAt_iff] at hs ht ⊢

Premises used: uniqueDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t
rw :
  Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F)) ∧
    (x, y) ∈ closure[inst_3] s ×ˢ closure[inst_8] t
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F)) ∧
    (x, y) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
rw [closure_prod_eq]

Premises used: closure_prod_eq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F)) ∧
    (x, y) ∈ closure[inst_3] s ×ˢ closure[inst_8] t

Tactic:
⟨?_, hs.2, ht.2⟩

Premises used: And.right, And.intro
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t
refine : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F))
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F)) ∧
    (x, y) ∈ closure[inst_3] s ×ˢ closure[inst_8] t

Tactic:
refine ⟨?_, hs.2, ht.2⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t
⊢ LE.le (α := Submodule 𝕜 (E × F))
    (Submodule.span 𝕜
      ((⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) '' tangentConeAt 𝕜 s x ∪
        (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) '' tangentConeAt 𝕜 t y))
    (Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))

Tactic:
have : _ ≤ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)) := Submodule.span_mono
    (union_subset (subset_tangentConeAt_prod_left ht.2) (subset_tangentConeAt_prod_right hs.2))
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t
this :
  LE.le (α := Submodule 𝕜 (E × F))
    (Submodule.span 𝕜
      ((⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) '' tangentConeAt 𝕜 s x ∪
        (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) '' tangentConeAt 𝕜 t y))
    (Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
⊢ ∀ ⦃x_1 : E × F⦄,
    Membership.mem (γ := Submodule 𝕜 (E × F))
        (Submodule.prod (Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) (Submodule.span 𝕜 (tangentConeAt 𝕜 t y))) x_1 →
      Membership.mem (γ := Submodule 𝕜 (E × F)) (Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) x_1

Tactic:
rw [LinearMap.span_inl_union_inr, SetLike.le_def] at this

Premises used: LinearMap.span_inl_union_inr, SetLike.le_def