awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds_1 : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot
hcd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
this :
  Tendsto (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ y ∈ tangentConeAt R s x
have rw : Membership.mem (γ := Set E)
  {y : E | ClusterPt y (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))}
  y
Tactic: rw [tangentConeAt_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
⊢ y ∈ tangentConeAt R s x
have suffices : Tendsto (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
  (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
Tactic: suffices Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(x + ·) ⁻¹' s] 0) by
    rw [frequently_iff_neBot] at hds
    rw [tangentConeAt_def]
    exact ClusterPt.mono (hcd.mono_left inf_le_left).mapClusterPt this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
have rw : Tendsto.{u_1, v} (β := E) (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
  (map (fun (p : R × E) ↦ p.1 • p.2)
    (SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)))
Tactic: rw [← map₂_smul, ← map_prod_eq_map₂]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
⊢ Tendsto.{u_1, v} (β := E) (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (map (fun (p : R × E) ↦ p.1 • p.2)
      (SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)))
have refine_1 : Tendsto d (l ⊓ 𝓟 {y : α | x + d y ∈ s}) (𝓝 0)
Tactic: refine tendsto_map.comp (tendsto_top.prodMk (tendsto_nhdsWithin_iff.mpr ⟨?_, ?_⟩))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
refine_1 : Tendsto d (l ⊓ 𝓟 {y : α | x + d y ∈ s}) (𝓝 0)
⊢ Tendsto.{u_1, v} (β := E) (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (map (fun (p : R × E) ↦ p.1 • p.2)
      (SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)))
have refine_2 : ∀ᶠ (n : α) in l ⊓ 𝓟 {y : α | x + d y ∈ s}, Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) (d n)
Tactic: refine tendsto_map.comp (tendsto_top.prodMk (tendsto_nhdsWithin_iff.mpr ⟨?_, ?_⟩))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (hypothesis)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h : y ∈ tangentConeAt R s x
⊢ ∃ (α : Type (max u v)) (l : Filter α) (_ : l.NeBot) (c : α → R) (d : α → E),
    Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
have h₁ : (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
    SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
Tactic: rw [tangentConeAt, mem_setOf, ← map₂_smul, ← map_prod_eq_map₂, ClusterPt,
    ← neBot_inf_comap_iff_map'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∃ (α : Type (max u v)) (l : Filter α) (_ : l.NeBot) (c : α → R) (d : α → E),
    Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
have refine_1 : Tendsto Prod.snd
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
    SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
  (𝓝 0)
Tactic: refine ⟨R × E, _, h, Prod.fst, Prod.snd, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
refine_1 :
  Tendsto Prod.snd
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 0)
⊢ ∃ (α : Type (max u v)) (l : Filter α) (_ : l.NeBot) (c : α → R) (d : α → E),
    Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
have refine_2 : ∀ᶠ (n : R × E) in
  comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
    SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
  x + n.2 ∈ s
Tactic: refine ⟨R × E, _, h, Prod.fst, Prod.snd, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
refine_1 :
  Tendsto Prod.snd
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 0)
refine_2 :
  ∀ᶠ (n : R × E) in
    comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + n.2 ∈ s
⊢ ∃ (α : Type (max u v)) (l : Filter α) (_ : l.NeBot) (c : α → R) (d : α → E),
    Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
have refine_3 : Tendsto (fun (n : R × E) ↦ n.1 • n.2)
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
    SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
  (𝓝 y)
Tactic: refine ⟨R × E, _, h, Prod.fst, Prod.snd, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ Tendsto Prod.snd
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 0)
have refine_1 : SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
  SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝 0)
Tactic: refine (tendsto_snd (f := ⊤)).mono_left <| inf_le_right.trans <| ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝 0)
have refine_1 : LE.le (α := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝 0)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∀ᶠ (n : R × E) in
    comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + n.2 ∈ s
have refine_2 : ∀ᶠ (x_1 : R × E) in SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0), x + x_1.2 ∈ s
Tactic: refine .filter_mono inf_le_right ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∀ᶠ (x_1 : R × E) in SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + x_1.2 ∈ s
have refine_2 : ∀ᶠ (b : E) in 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0, ∀ (a : R × E), a.2 = b → x + a.2 ∈ s
Tactic: rw [top_prod, eventually_comap]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∀ᶠ (b : E) in 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0, ∀ (a : R × E), a.2 = b → x + a.2 ∈ s
have h₁ : ∀ (a : E), Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) a → ∀ (a_2 : R × E), a_2.2 = a → x + a_2.2 ∈ s
Tactic: filter_upwards [eventually_mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.DimOne (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
⊢ tangentConeAt 𝕜 s x = univ
have refine : ∀ (y : 𝕜), y ∈ tangentConeAt 𝕜 s x
Tactic: refine eq_univ_of_forall fun y ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.DimOne (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ y ∈ tangentConeAt 𝕜 s x
have hd₀ : Tendsto (β := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (𝓝[≠] x) (𝓝 0)
Tactic: apply mem_tangentConeAt_of_frequently (𝓝[≠] x) (fun z ↦ y / (z - x)) (· - x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.DimOne (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
hd₀ : Tendsto (β := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (𝓝[≠] x) (𝓝 0)
⊢ y ∈ tangentConeAt 𝕜 s x
have hds : ∃ᶠ (n : 𝕜) in 𝓝[≠] x, x + (n - x) ∈ s
Tactic: apply mem_tangentConeAt_of_frequently (𝓝[≠] x) (fun z ↦ y / (z - x)) (· - x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.DimOne (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
hd₀ : Tendsto (β := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (𝓝[≠] x) (𝓝 0)
hds : ∃ᶠ (n : 𝕜) in 𝓝[≠] x, x + (n - x) ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x
have hcd : Tendsto (fun (n : 𝕜) ↦ (y / (n - x)) • (n - x)) (𝓝[≠] x) (𝓝 y)
Tactic: apply mem_tangentConeAt_of_frequently (𝓝[≠] x) (fun z ↦ y / (z - x)) (· - x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.DimOne (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ Tendsto (fun (n : 𝕜) ↦ (y / (n - x)) • (n - x)) (𝓝[≠] x) (𝓝 y)
have hcd : ∀ᶠ (x' : 𝕜) in 𝓝[≠] x, (y / (x' - x)) • (x' - x) = y
Tactic: apply tendsto_nhds_of_eventually_eq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.DimOne (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ ∀ᶠ (x' : 𝕜) in 𝓝[≠] x, (y / (x' - x)) • (x' - x) = y
have hcd : ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z), (y / (z - x)) • (z - x) = y
Tactic: refine eventually_mem_nhdsWithin.mono fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.DimOne (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ (y / (z - x)) • (z - x) = y
have this : z - x ≠ 0
Tactic: have : z - x ≠ 0 := by simpa [sub_eq_zero] using hz
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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
inst_6 : DecidableEq ι
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure[inst_3 j] (s j)
⊢ MapsTo (Pi.single (M := E) i) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)
have rw : MapsTo (Pi.single (M := E) i) (tangentConeAt 𝕜 (s i) (x i))
  (tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x)
Tactic: rw [← tangentConeAt_closure (s := .pi _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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
inst_6 : DecidableEq ι
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
⊢ Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x
have rcases : ∀ (ι_1 : Type (max u_1 u_3)) (l : Filter ι_1) (hl : l.NeBot) (c : ι_1 → 𝕜) (d : ι_1 → E i) (hd₀ : Tendsto d l (𝓝 0))
  (hds : ∀ᶠ (n : ι_1) in l, x i + d n ∈ s i) (hcd : Tendsto (fun (n : ι_1) ↦ c n • d n) l (𝓝 y)),
  Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x
Tactic: rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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)
⊢ Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x
have hd₁ : Tendsto (β := (j : ι_1) → E j) (fun (n : ι) ↦ Pi.single (M := E) i (d n)) l (𝓝 0)
Tactic: apply mem_tangentConeAt_of_seq l c (fun n ↦ Pi.single i (d n))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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)
⊢ Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x
have hds₁ : ∀ᶠ (n : ι) in l, x + Pi.single (M := E) i (d n) ∈ closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)
Tactic: apply mem_tangentConeAt_of_seq l c (fun n ↦ Pi.single i (d n))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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)
⊢ Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x
have hcd₁ : Tendsto (fun (n : ι) ↦ c n • Pi.single (M := E) i (d n)) l (𝓝 (Pi.single (M := E) i y))
Tactic: apply mem_tangentConeAt_of_seq l c (fun n ↦ Pi.single i (d n))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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)
⊢ Tendsto (β := (j : ι_1) → E j) (fun (n : ι) ↦ Pi.single (M := E) i (d n)) l (𝓝 0)
have hd₁ : ∀ (x : ι_1), Tendsto (β := E x) (fun (i_1 : ι) ↦ Pi.single (M := E) i (d i_1) x) l (𝓝 (0 x))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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
⊢ Tendsto (β := E j) (fun (i_1 : ι) ↦ Pi.single (M := E) i (d i_1) j) l (𝓝 (0 j))
have 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))
Tactic: rcases eq_or_ne j i with rfl | hj
Cleared hypotheses: i, hi, y, hy, d, hd₀, hds, hcd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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))
⊢ Tendsto (β := E j) (fun (i_1 : ι) ↦ Pi.single (M := E) i (d i_1) j) l (𝓝 (0 j))
have hd₂ : ∀ (hj : j ≠ i), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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)
have 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)
Tactic: refine hds.mono fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
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
⊢ x + Pi.single (M := E) i (d n) ∈ closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)
have hds₁ : ∀ (i_1 : ι_1), (x + Pi.single (M := E) i (d n)) i_1 ∈ closure[inst_3 i_1] (s i_1)
Tactic: rw [closure_pi_set, mem_univ_pi]