awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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 𝕜 (I.pi (α := E) s) x
have rw : UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s fun (x : ι) ↦ univ)) x
Tactic: rw [← Set.univ_pi_piecewise_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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
have refine : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
Tactic: refine UniqueDiffWithinAt.univ_pi fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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 : ι
⊢ UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
have pos : ∀ (hi : i ∈ I), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
Tactic: by_cases hi : i ∈ I
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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)
⊢ UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
have neg : ∀ (hi : i ∉ I), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
Tactic: by_cases hi : i ∈ I
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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 𝕜 (I.pi (α := E) s) x
have rw : UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s fun (x : ι) ↦ univ)) x
Tactic: classical
  rw [← Set.univ_pi_piecewise_univ]
  refine UniqueDiffWithinAt.univ_pi fun i => ?_
  by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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
⊢ UniqueDiffWithinAt 𝕜 (I.pi (α := E) s) x
have rw₃ : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (I.piecewise (β := fun (i : ι) ↦ Set (E i)) s (fun (x : ι) ↦ univ) i) (x i)
Tactic: classical
  rw [← Set.univ_pi_piecewise_univ]
  refine UniqueDiffWithinAt.univ_pi fun i => ?_
  by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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
⊢ (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
have rw : (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) '' tangentConeAt 𝕜 s x ⊆
  tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y)
Tactic: rw [← tangentConeAt_closure (s := s ×ˢ t), closure_prod_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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
⊢ 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)
have 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)
Tactic: rcases exists_fun_of_mem_tangentConeAt hz with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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)
⊢ 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)
have 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))
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]) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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
⊢ (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
have rw : (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) '' tangentConeAt 𝕜 t y ⊆
  tangentConeAt 𝕜 (closure[inst_3] s ×ˢ closure[inst_8] t) (x, y)
Tactic: rw [← tangentConeAt_closure (s := s ×ˢ t), closure_prod_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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
⊢ 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)
have 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)
Tactic: rcases exists_fun_of_mem_tangentConeAt hz with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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)
⊢ 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)
have 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))
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]) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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
⊢ UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)
have 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)
Tactic: rw [uniqueDiffWithinAt_iff] at hs ht ⊢
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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[instTopologicalSpaceProd] (s ×ˢ t)
have rw : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F)) ∧
  (x, y) ∈ closure[inst_3] s ×ˢ closure[inst_8] t
Tactic: rw [closure_prod_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (goal)
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
have refine : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F))
Tactic: refine ⟨?_, hs.2, ht.2⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (hypothesis)
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))
have 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)))
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))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Prod (hypothesis)
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)))
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F))
have this₁ : ∀ ⦃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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have obtain : ∀ (u : ℕ → ℝ) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
Tactic: obtain ⟨u, -, u_pos, u_lim⟩ :
      ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have A : ∀ (n : ℕ), ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x
Tactic: have A n : ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x :=
    accPt_iff_nhds.mp hx _ (closedBall_mem_nhds _ (u_pos n))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
A : ∀ (n : ℕ), ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have choose : ∀ (v : (n : ℕ) → E) (hv : ∀ (n : ℕ), v n ∈ closedBall x (u n) ∩ s) (hvx : ∀ (n : ℕ), v n ≠ x),
  (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
Tactic: choose v hv hvx using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hv : ∀ (n : ℕ), v n ∈ closedBall x (u n) ∩ s
hvx : ∀ (n : ℕ), v n ≠ x
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
Tactic: choose hvu hvs using hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hv : ∀ (n : ℕ), v n ∈ closedBall x (u n) ∩ s
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have hvs : ∀ (n : ℕ), v n ∈ s
Tactic: choose hvu hvs using hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have M : ∀ (n : ℕ), x + d n ∈ s \ {x}
Tactic: have M n : x + d n ∈ s \ {x} := by simp [d, hvs, hvx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have let : ∀ (r : 𝕜) (hr : 1 < ‖r‖), (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
Tactic: let ⟨r, hr⟩ := exists_one_lt_norm 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have W : ∀ (n : ℕ), ∃ (d_1 : 𝕜), d_1 ≠ 0 ∧ ‖d_1 • d n‖ < 1 ∧ 1 / ‖r‖ ≤ ‖d_1 • d n‖ ∧ ‖d_1‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
Tactic: have W n := rescale_to_shell hr zero_lt_one (x := d n) (by simpa using (M n).2)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
W : ∀ (n : ℕ), ∃ (d_1 : 𝕜), d_1 ≠ 0 ∧ ‖d_1 • d n‖ < 1 ∧ 1 / ‖r‖ ≤ ‖d_1 • d n‖ ∧ ‖d_1‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have choose : ∀ (c : (n : ℕ) → 𝕜) (c_ne : ∀ (n : ℕ), c n ≠ 0) (c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1)
  (le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖) (hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖),
  (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
Tactic: choose c c_ne c_le le_c hc using W
Cleared hypotheses: W
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
⊢ ∃ (l : E),
    Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l ∧
      ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
have apply : IsCompact.{u_2} (X := E) (closedBall 0 1 \ ball 0 (1 / ‖r‖))
Tactic: apply IsCompact.tendsto_subseq _ (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.ProperSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
apply : IsCompact.{u_2} (X := E) (closedBall 0 1 \ ball 0 (1 / ‖r‖))
⊢ ∃ (l : E),
    Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l ∧
      ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
have apply₁ : ∀ (n : ℕ), Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) (c n • d n)
Tactic: apply IsCompact.tendsto_subseq _ (fun n ↦ ?_)