awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
apply : ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) 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)

Tactic:
apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add

Premises used: ContDiff.sum, ContDiff.of_le, ContDiff.add
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
⊢ ∀ (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 _
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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

Tactic:
contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_

Premises used: WithTop.coe_le_coe._simp_1, cast, ContDiff.of_le, contDiff_tsum, Eq.symm, Subtype.val
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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))
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
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x

Tactic:
refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_

Premises used: ContDiff.of_le, contDiff_tsum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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 : ℕ∞)
⊢ ∀ 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

Premises used: not_le, Set.Finite.mem_toFinset, not_exists, Set.mem_setOf_eq, Finset.mem_range, exists_prop, not_lt, not_and, Classical.not_forall
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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_1 : i ∉ T
x : E
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞)
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
⊢ 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_1) : α)) x) ≤
    comp (α := { i : α // i ∉ T }) (v k) (Subtype.val (p := fun (i : α) ↦ i ∉ T))
      (Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi_1)

Tactic:
hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x

Premises used: Iff.mpr, Nat.lt_succ_iff, Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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_1 : i ∉ T
x : E
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞)
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
⊢ 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_1) : α)) x) ≤
    comp (α := { i : α // i ∉ T }) (v k) (Subtype.val (p := fun (i : α) ↦ i ∉ T))
      (Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi_1)

Tactic:
exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x

Premises used: Iff.mpr, Nat.lt_succ_iff, Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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))
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Tactic:
simp only [tangentConeAt_def, setOf_subset_setOf]

Premises used: tangentConeAt_def, Set.setOf_subset_setOf
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))

Tactic:
fun y hy ↦ hy.mono ?_

Premises used: ClusterPt.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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)
⊢ ∀ (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:
refine fun y hy ↦ hy.mono ?_
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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:
gcongr
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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))
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x

Tactic:
simp only [tangentConeAt_def, setOf_subset_setOf]

Premises used: tangentConeAt_def, Set.setOf_subset_setOf
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))

Tactic:
fun y hy ↦ hy.mono ?_

Premises used: ClusterPt.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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)
⊢ ∀ (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:
refine fun y hy ↦ hy.mono ?_
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))
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)
⊢ 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:
rw [← smul_one_smul (Filter 𝕜')]

Premises used: smul_one_smul, Filter
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))
grw 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)
⊢ 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:
grw [le_top (a := ⊤ • 1)]

Premises used: le_top
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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
⊢ 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))

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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:
simp only [tangentConeAt_def, mem_setOf_eq, mem_iInter₂, ← map₂_smul, ← map_prod_eq_map₂,
    ((nhdsWithin_hasBasis h _).top_prod.map _).clusterPt_iff_forall_mem_closure, image_prod,
    image2_smul]

Premises used: Filter.map₂_smul, Set.image_prod, Set.mem_iInter₂, Filter.HasBasis.map, Set.mem_setOf_eq, tangentConeAt_def, Filter.map_prod_eq_map₂, Set.image2_smul, Filter.HasBasis.top_prod, nhdsWithin_hasBasis, Filter.HasBasis.clusterPt_iff_forall_mem_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
⊢ tangentConeAt 𝕜 s x =
    ⋂ (U : Set E),
      ⋂ (_ : Membership.mem (γ := Filter E) (𝓝 0) U),
        closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))

Tactic:
(basis_sets _).tangentConeAt_eq_biInter_closure

Premises used: Filter.basis_sets, Filter.HasBasis.tangentConeAt_eq_biInter_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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))
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Tactic:
simp only [tangentConeAt_def, setOf_subset_setOf]

Premises used: tangentConeAt_def, Set.setOf_subset_setOf
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))

Tactic:
fun y hy ↦ hy.mono ?_

Premises used: ClusterPt.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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)
⊢ ∀ (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:
refine fun y hy ↦ hy.mono ?_
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))
h₁ : LE.le (α := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 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:
gcongr _ • ?_
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))
h₁ : Membership.mem (γ := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' t)
⊢ LE.le (α := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' t] 0)

Tactic:
rw [nhdsWithin_le_iff]

Premises used: nhdsWithin_le_iff