awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have obtain : ∀ (l : E) (l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l) (φ : ℕ → ℕ)
  (φ_strict : StrictMono φ) (hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)),
  (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
Tactic: obtain ⟨l, l_mem, φ, φ_strict, hφ⟩ :
      ∃ l ∈ Metric.closedBall (0 : E) 1 \ Metric.ball (0 : E) (1 / ‖r‖),
      ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l) := by
    apply IsCompact.tendsto_subseq _ (fun n ↦ ?_)
    · exact (isCompact_closedBall 0 1).diff Metric.isOpen_ball
    simp only [mem_diff, Metric.mem_closedBall, dist_zero_right, (c_le n).le,
      Metric.mem_ball, not_lt, true_and, le_c 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‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have refine_1 : l ∈ tangentConeAt 𝕜 s x
Tactic: refine ⟨l, ?_, ?_⟩
-- 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
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
refine_1 : l ∈ tangentConeAt 𝕜 s x
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
have refine_2 : Membership.mem (γ := Set E) {0}ᶜ l
Tactic: refine ⟨l, ?_, ?_⟩
-- 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
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ¬l = 0
have refine_2 : ∀ (l_mem : l = 0), l ∉ closedBall 0 1 \ ball 0 (1 / ‖r‖)
Tactic: contrapose l_mem
Cleared hypotheses: l_mem
-- 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
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
l_mem : l = 0
⊢ l ∉ closedBall 0 1 \ ball 0 (1 / ‖r‖)
have refine_2 : ¬r = 0
Tactic: simp only [one_div, l_mem, mem_diff, Metric.mem_closedBall, dist_self, zero_le_one,
      Metric.mem_ball, inv_pos, norm_pos_iff, ne_eq, not_not, true_and]
-- 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
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
l_mem : l = 0
⊢ ¬r = 0
have refine_2 : ∀ (hr : r = 0), ‖r‖ ≤ 1
Tactic: contrapose! hr
Cleared hypotheses: hr
-- 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
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ l ∈ tangentConeAt 𝕜 s x
have refine_1 : Tendsto (d ∘ φ) atTop (𝓝 0)
Tactic: apply mem_tangentConeAt_of_seq atTop (c ∘ φ) (d ∘ φ)
-- 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
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
refine_1 : Tendsto (d ∘ φ) atTop (𝓝 0)
⊢ l ∈ tangentConeAt 𝕜 s x
have refine_1₁ : ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s
Tactic: apply mem_tangentConeAt_of_seq atTop (c ∘ φ) (d ∘ φ)
-- 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
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
refine_1 : Tendsto (d ∘ φ) atTop (𝓝 0)
refine_1₁ : ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s
⊢ l ∈ tangentConeAt 𝕜 s x
have refine_1₂ : Tendsto (fun (n : ℕ) ↦ (c ∘ φ) n • (d ∘ φ) n) atTop (𝓝 l)
Tactic: apply mem_tangentConeAt_of_seq atTop (c ∘ φ) (d ∘ φ)
-- 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
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (d ∘ φ) atTop (𝓝 0)
have refine_1 : Tendsto d atTop (𝓝 0)
Tactic: refine Tendsto.comp ?_ φ_strict.tendsto_atTop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
⊢ y - x ∈ tangentConeAt ℝ≥0 s x
have refine : ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0, x + id n • (y - x) ∈ s
Tactic: refine mem_tangentConeAt_of_add_smul_mem (tendsto_id'.mpr <| nhdsGT_le_nhdsNE 0) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
⊢ ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0, x + id n • (y - x) ∈ s
have h₁ : ∀ (a : ℝ≥0) (ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a), x + id a • (y - x) ∈ s
Tactic: filter_upwards [Ioo_mem_nhdsGT one_pos] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a
⊢ x + id a • (y - x) ∈ s
have h₁ : x + id a • (y - x) ∈ openSegment ℝ x y
Tactic: apply h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a
⊢ x + id a • (y - x) ∈ openSegment ℝ x y
have h₁ : Membership.mem (γ := Set E) (image (α := ℝ) (⇑(AffineMap.lineMap x y) : (a : ℝ) → E) (Ioo 0 1)) (x + id a • (y - x))
Tactic: rw [openSegment_eq_image_lineMap]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a
⊢ Membership.mem (γ := Set E) (image (α := ℝ) (⇑(AffineMap.lineMap x y) : (a : ℝ) → E) (Ioo 0 1)) (x + id a • (y - x))
have right : (AffineMap.lineMap x y : (a : ℝ) → E) (↑a : ℝ) = x + id a • (y - x)
Tactic: use a, mod_cast ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hs : (interior s).Nonempty
hx : x ∈ closure[inst_2] s
⊢ Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤
have rcases : ∀ (y : E) (hy : y ∈ interior s), Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤
Tactic: rcases hs with ⟨y, hy⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤
have apply : (interior (↑(Submodule.span ℝ (tangentConeAt ℝ s x)) : Set E)).Nonempty
Tactic: apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
⊢ Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤
have suffices : y - x ∈ interior (tangentConeAt ℝ s x)
Tactic: suffices y - x ∈ interior (tangentConeAt ℝ s x) by
    apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
    exact ⟨y - x, interior_mono Submodule.subset_span this⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
⊢ y - x ∈ interior (tangentConeAt ℝ s x)
have rw : tangentConeAt ℝ s x ∈ 𝓝 (y - x)
Tactic: rw [mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)
have hy₁ : interior s ∈ 𝓝 y
Tactic: replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : interior s ∈ 𝓝 y
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)
have apply : (fun (x_1 : E) ↦ x_1 - x) '' interior s ⊆ tangentConeAt ℝ s x
Tactic: apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Real (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : interior s ∈ 𝓝 y
z : E
zs : z ∈ interior s
⊢ (fun (x_1 : E) ↦ x_1 - x) z ∈ tangentConeAt ℝ s x
have refine : openSegment ℝ x z ⊆ interior s
Tactic: refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
⊢ y ∈ tangentConeAt R s x ↔
    ∃ (c : ℕ → R) (d : ℕ → E),
      Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have mp : y ∈ tangentConeAt R s x →
  ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
mp :
  y ∈ tangentConeAt R s x →
    ∃ (c : ℕ → R) (d : ℕ → E),
      Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt R s x ↔
    ∃ (c : ℕ → R) (d : ℕ → E),
      Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have mpr : (∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)) →
  y ∈ tangentConeAt R s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
h : y ∈ tangentConeAt R s x
⊢ ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 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: simp only [tangentConeAt_def, Set.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.Seq (goal)
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology 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
⊢ ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have mp : ∀ (cd : ℕ → R × E)
  (hcd :
    Tendsto cd atTop
      (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))),
  ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
Tactic: rcases @exists_seq_tendsto _ _ _ h with ⟨cd, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology 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
cd : ℕ → R × E
hcd :
  Tendsto cd atTop
    (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))
⊢ ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have hcd₁ : Tendsto ((fun (p : R × E) ↦ p.1 • p.2) ∘ cd) atTop (𝓝 y) ∧
  Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ (cd n).1) atTop ⊤ ∧
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ (cd n).2) atTop (𝓝 0) ∧
      ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) (cd n).2
Tactic: simp only [tendsto_inf, tendsto_comap_iff, tendsto_prod_iff', tendsto_nhdsWithin_iff] at hcd
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
α : Type u_3
l : Filter α
c : α → 𝕜
d : α → E
y : E
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
hd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
⊢ Tendsto d l (𝓝 0)
have this : ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n
Tactic: have : ∀ᶠ n in l, (c n)⁻¹ • c n • d n = d n :=
    (eventually_ne_of_tendsto_norm_atTop hc 0).mono fun n hn ↦ inv_smul_smul₀ hn (d n)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
α : Type u_3
l : Filter α
c : α → 𝕜
d : α → E
y : E
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
hd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
this : ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n
⊢ Tendsto d l (𝓝 0)
have hc₁ : Tendsto c l (Bornology.cobounded 𝕜)
Tactic: rw [tendsto_norm_atTop_iff_cobounded] at hc
Cleared hypotheses: hc, hd, this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
x y : E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x
have refine : ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set 𝕜) {0}ᶜ (r ^ n)
Tactic: refine mem_tangentConeAt_of_add_smul_mem
    (tendsto_nhdsWithin_iff.mpr ⟨tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr, ?_⟩) hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
⊢ y ∈ tangentConeAt 𝕜 s x ↔
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have mp : y ∈ tangentConeAt 𝕜 s x →
  ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
mp :
  y ∈ tangentConeAt 𝕜 s x →
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 s x ↔
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have mpr : (∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)) →
  y ∈ tangentConeAt 𝕜 s x
Tactic: constructor