awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
this :
  (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
have rw : ContDiff 𝕜 (↑m : WithTop ℕ∞)
  (HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
this :
  (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
⊢ ContDiff 𝕜 (↑m : WithTop ℕ∞)
    (HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦
      ∑' (i : { i : α // i ∉ T }), f (↑i : α) x)
have apply : ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
Tactic: apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
this :
  (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
have h'u : ∀ (k : ℕ),
  LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
    Summable (β := { i : α // i ∉ T }) (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T))
Tactic: have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
      (hv k (hk.trans hm)).subtype _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
this :
  (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
h'u :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
      Summable (β := { i : α // i ∉ T }) (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T))
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
have refine : ∀ (k : ℕ) (i : { i : α // i ∉ T }) (x : E),
  LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
    norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
        (iteratedFDeriv 𝕜 k (f (↑i : α)) x) ≤
      (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T)) i
Tactic: refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
this :
  (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
h'u :
  ∀ (k : ℕ),
    LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
      Summable (β := { i : α // i ∉ T }) (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T))
k : ℕ
i : α
hi : i ∉ T
x : E
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞)
⊢ norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k (f (↑(Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi) : α)) x) ≤
    comp (α := { i : α // i ∉ T }) (v k) (Subtype.val (p := fun (i : α) ↦ i ∉ T))
      (Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi)
have hi₁ : ∀ x < m + 1,
  ∀ (x_1 : E),
    norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin x) ↦ E) F) (iteratedFDeriv 𝕜 x (f i) x_1) ≤
      v x i
Tactic: simp only [t, T, Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le,
      exists_prop, not_exists, not_and, not_lt] at hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
have refine : ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
Tactic: classical
    refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
    let t : Set α :=
      { i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i }
    have ht : Set.Finite t :=
      haveI A :
        ∀ᶠ i in (Filter.cofinite : Filter α),
          ∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i := by
        rw [eventually_all_finset]
        intro i hi
        apply h'f
        simp only [Finset.mem_range_succ_iff] at hi
        exact (WithTop.coe_le_coe.2 hi).trans hm
      eventually_cofinite.2 A
    let T : Finset α := ht.toFinset
    have : (fun x => ∑' i, f i x) = (fun x => ∑ i ∈ T, f i x) +
        fun x => ∑' i : { i // i ∉ T }, f i x := by
      ext1 x
      refine (Summable.sum_add_tsum_subtype_compl ?_ T).symm
      refine .of_norm_bounded_eventually (hv 0 zero_le) ?_
      filter_upwards [h'f 0 zero_le] with i hi
      simpa only [norm_iteratedFDeriv_zero] using hi x
    rw [this]
    apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add
    have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
      (hv k (hk.trans hm)).subtype _
    refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_
    rintro k ⟨i, hi⟩ x hk
    simp only [t, T, Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le,
      exists_prop, not_exists, not_and, not_lt] at hi
    exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
refine :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
refine₁ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
have refine₂ : ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
  let t : Set α :=
    {i : α |
      ¬∀ k ∈ Finset.range (m + 1),
          ∀ (x : E),
            norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
                (iteratedFDeriv 𝕜 k (f i) x) ≤
              v k i};
  ∀ (ht : t.Finite), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
Tactic: classical
    refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
    let t : Set α :=
      { i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i }
    have ht : Set.Finite t :=
      haveI A :
        ∀ᶠ i in (Filter.cofinite : Filter α),
          ∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i := by
        rw [eventually_all_finset]
        intro i hi
        apply h'f
        simp only [Finset.mem_range_succ_iff] at hi
        exact (WithTop.coe_le_coe.2 hi).trans hm
      eventually_cofinite.2 A
    let T : Finset α := ht.toFinset
    have : (fun x => ∑' i, f i x) = (fun x => ∑ i ∈ T, f i x) +
        fun x => ∑' i : { i // i ∉ T }, f i x := by
      ext1 x
      refine (Summable.sum_add_tsum_subtype_compl ?_ T).symm
      refine .of_norm_bounded_eventually (hv 0 zero_le) ?_
      filter_upwards [h'f 0 zero_le] with i hi
      simpa only [norm_iteratedFDeriv_zero] using hi x
    rw [this]
    apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add
    have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
      (hv k (hk.trans hm)).subtype _
    refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_
    rintro k ⟨i, hi⟩ x hk
    simp only [t, T, Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le,
      exists_prop, not_exists, not_and, not_lt] at hi
    exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
h : s ⊆ t
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x
have simp : ∀ (a : E),
  ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)) →
    ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0))
Tactic: simp only [tangentConeAt_def, setOf_subset_setOf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
h : s ⊆ t
⊢ ∀ (a : E),
    ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)) →
      ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0))
have refine : ∀ (y : E)
  (hy :
    ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))),
  HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0)
Tactic: refine fun y hy ↦ hy.mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst_3 : Monoid 𝕜'
inst_4 : SMul 𝕜 𝕜'
inst_5 : MulAction 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x
have simp : ∀ (a : E),
  ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)) →
    ClusterPt a (HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
Tactic: simp only [tangentConeAt_def, setOf_subset_setOf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst_3 : Monoid 𝕜'
inst_4 : SMul 𝕜 𝕜'
inst_5 : MulAction 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ ∀ (a : E),
    ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)) →
      ClusterPt a
        (HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
have refine : ∀ (y : E)
  (hy :
    ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))),
  HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)
Tactic: refine fun y hy ↦ hy.mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst_3 : Monoid 𝕜'
inst_4 : SMul 𝕜 𝕜'
inst_5 : MulAction 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)
have rw : HSMul.hSMul (β := Filter E) (HSMul.hSMul.{u_1, u_3, u_3} (α := Filter 𝕜) (β := Filter 𝕜') ⊤ 1)
    (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
  HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)
Tactic: rw [← smul_one_smul (Filter 𝕜')]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst_3 : Monoid 𝕜'
inst_4 : SMul 𝕜 𝕜'
inst_5 : MulAction 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ HSMul.hSMul (β := Filter E) (HSMul.hSMul.{u_1, u_3, u_3} (α := Filter 𝕜) (β := Filter 𝕜') ⊤ 1)
      (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)
have grw : HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
  HSMul.hSMul.{u_3, u_2, u_2} (α := Filter 𝕜') (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)
Tactic: grw [le_top (a := ⊤ • 1)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
ι : Sort u_3
p : ι → Prop
U : ι → Set E
h : HasBasis (𝓝 0) p U
⊢ tangentConeAt 𝕜 s x =
    ⋂ (i : ι),
      ⋂ (_ : p i),
        closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U i ∩ (fun (x_2 : E) ↦ x + x_2) ⁻¹' s))
have h₁ : ∀ (y : E),
  y ∈ tangentConeAt 𝕜 s x ↔
    Membership.mem (γ := Set E)
      (⋂ (i : ι),
        ⋂ (_ : p i),
          closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U i ∩ (fun (x_2 : E) ↦ x + x_2) ⁻¹' s)))
      y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x
have simp : ∀ (a : E),
  ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)) →
    ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0))
Tactic: simp only [tangentConeAt_def, setOf_subset_setOf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
⊢ ∀ (a : E),
    ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)) →
      ClusterPt a (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0))
have refine : ∀ (y : E)
  (hy :
    ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))),
  HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0)
Tactic: refine fun y hy ↦ hy.mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0)
have h₁ : LE.le (α := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0)
Tactic: gcongr _ • ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ LE.le (α := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0)
have h₁ : Membership.mem (γ := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' t)
Tactic: rw [nhdsWithin_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ Membership.mem (γ := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' t)
have h₁ : Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[s] x)
Tactic: suffices Tendsto (x + ·) (𝓝[(x + ·) ⁻¹' s] 0) (𝓝[s] x) from
    this.mono_right h |> tendsto_nhdsWithin_iff.mp |>.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[s] x)
have h₁ : Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝 0) (𝓝 x)
Tactic: refine .inf ?_ (mapsTo_preimage _ _).tendsto
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
h : (tangentConeAt 𝕜 s x).Nonempty
⊢ x ∈ closure[inst_2] s
have rcases : ∀ (y : E) (hy : y ∈ tangentConeAt 𝕜 s x), x ∈ closure[inst_2] s
Tactic: rcases h with ⟨y, hy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
y : E
hy : y ∈ tangentConeAt 𝕜 s x
⊢ x ∈ closure[inst_2] s
have rcases : ∀ (ι : Type (max u_1 u_2)) (l : Filter ι) (hl : l.NeBot) (d : ι → E) (hd : Tendsto d l (𝓝 0))
  (hds : ∀ᶠ (n : ι) in l, x + d n ∈ s), x ∈ closure[inst_2] s
Tactic: rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, -, d, hd, hds, -⟩