awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Tendsto.{u_1, 0} (α := List α) length (pure []) (pure (length.{u_1} (α := α) []))

Tactic:
exact tendsto_pure_pure _ _

Premises used: Filter.tendsto_pure_pure
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun (p : α × List α) ↦ p.2.length + 1) (𝓝 a ×ˢ 𝓝 l) (pure (l.length + 1))

Tactic:
Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) ?_

Premises used: Filter.tendsto_pure_pure, HAdd.hAdd, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
refine_2 : Tendsto (fun (p : α × List α) ↦ p.2.length.add 0) (𝓝 a ×ˢ 𝓝 l) (pure l.length)
⊢ Tendsto (fun (p : α × List α) ↦ p.2.length + 1) (𝓝 a ×ˢ 𝓝 l) (pure (l.length + 1))

Tactic:
refine Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) ?_

Premises used: Filter.tendsto_pure_pure, HAdd.hAdd, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun (p : α × List α) ↦ p.2.length.add 0) (𝓝 a ×ˢ 𝓝 l) (pure l.length)

Tactic:
Tendsto.comp ih tendsto_snd

Premises used: Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun (p : α × List α) ↦ p.2.length.add 0) (𝓝 a ×ˢ 𝓝 l) (pure l.length)

Tactic:
exact Tendsto.comp ih tendsto_snd

Premises used: Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
⊢ Tendsto (fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) (SProd.sprod (β := Filter (List α)) (𝓝 a) (𝓝 []))
    (𝓝 (insertIdx [] (n + 1) a))

Tactic:
simp
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
simp :
  Eq (α := Filter (α × List α)) (Prod.mk <$> 𝓝 a <*> (cons <$> 𝓝 a' <*> 𝓝 l))
    ((fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) <$> (Prod.mk <$> 𝓝 a <*> (Prod.mk <$> 𝓝 a' <*> 𝓝 l)))
⊢ 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)

Tactic:
simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]

Premises used: Filter.prod_eq, nhds_cons, Filter.seq_eq_filter_seq, Filter.map_def
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Eq (α := Filter (α × List α)) (Prod.mk <$> 𝓝 a <*> (cons <$> 𝓝 a' <*> 𝓝 l))
    ((fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) <$> (Prod.mk <$> 𝓝 a <*> (Prod.mk <$> 𝓝 a' <*> 𝓝 l)))

Tactic:
simp [-Filter.map_def, Function.comp_def, functor_norm]

Premises used: Function.comp_def, Filter.map_def
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)

Tactic:
have : 𝓝 a ×ˢ 𝓝 (a'::l) =
        (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1::p.2.2) := by
      simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
      simp [-Filter.map_def, Function.comp_def, functor_norm]
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
rw :
  Tendsto ((fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) ∘ fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2))
    (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l) (𝓝 ((a' :: l).insertIdx (n + 1) a))
⊢ Tendsto (fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 ((a' :: l).insertIdx (n + 1) a))

Tactic:
rw [this, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) ∘ fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2))
    (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l) (𝓝 ((a' :: l).insertIdx (n + 1) a))

Tactic:
(tendsto_fst.comp tendsto_snd).cons
        ((@tendsto_insertIdx' _ n l).comp <| tendsto_fst.prodMk <| tendsto_snd.comp tendsto_snd)

Premises used: List.insertIdx, Filter.Tendsto.prodMk, List.modifyTailIdx.go, List.modifyTailIdx, Filter.Tendsto.cons, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) ∘ fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2))
    (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l) (𝓝 ((a' :: l).insertIdx (n + 1) a))

Tactic:
exact
      (tendsto_fst.comp tendsto_snd).cons
        ((@tendsto_insertIdx' _ n l).comp <| tendsto_fst.prodMk <| tendsto_snd.comp tendsto_snd)

Premises used: Filter.Tendsto.prodMk, Filter.Tendsto.cons, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
n : ℕ
a : α
l : List α
f : β → α
g : β → List α
b : Filter β
hf : Tendsto f b (𝓝 a)
hg : Tendsto g b (𝓝 l)
⊢ Tendsto (fun (b : β) ↦ (g b).insertIdx n (f b)) b (𝓝 (l.insertIdx n a))

Tactic:
tendsto_insertIdx'.comp (hf.prodMk hg)

Premises used: List.insertIdx, List.tendsto_insertIdx', Filter.Tendsto.prodMk, List.modifyTailIdx, Filter.Tendsto.comp
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
x : α × List α
a : α
l : List α
rw : Tendsto (fun (p : α × List α) ↦ p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a, l).2.insertIdx n (a, l).1))
⊢ ContinuousAt (Y := List α) (fun (p : α × List α) ↦ p.2.insertIdx n p.1) (a, l)

Tactic:
rw [ContinuousAt, nhds_prod_eq]

Premises used: ContinuousAt, nhds_prod_eq
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
x : α × List α
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a, l).2.insertIdx n (a, l).1))

Tactic:
tendsto_insertIdx'

Premises used: List.tendsto_insertIdx'
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
x : α × List α
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a, l).2.insertIdx n (a, l).1))

Tactic:
exact tendsto_insertIdx'

Premises used: List.tendsto_insertIdx'
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
x : ℕ
rw : Tendsto (β := List α) (fun (x_1 : List α) ↦ x_1.eraseIdx x) (pure []) (𝓝 (eraseIdx [] x))
⊢ Tendsto (β := List α) (fun (x_1 : List α) ↦ x_1.eraseIdx x) (𝓝 []) (𝓝 (eraseIdx [] x))

Tactic:
rw [nhds_nil]

Premises used: nhds_nil
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
x : ℕ
⊢ Tendsto (β := List α) (fun (x_1 : List α) ↦ x_1.eraseIdx x) (pure []) (𝓝 (eraseIdx [] x))

Tactic:
tendsto_pure_nhds _ _

Premises used: tendsto_pure_nhds
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
x : ℕ
⊢ Tendsto (β := List α) (fun (x_1 : List α) ↦ x_1.eraseIdx x) (pure []) (𝓝 (eraseIdx [] x))

Tactic:
exact tendsto_pure_nhds _ _

Premises used: tendsto_pure_nhds
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
rw : Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))
⊢ Tendsto (fun (x : List α) ↦ x.eraseIdx 0) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
rw [tendsto_cons_iff]

Premises used: List.tendsto_cons_iff
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
tendsto_snd

Premises used: List.eraseIdx, Filter.tendsto_snd
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
exact tendsto_snd

Premises used: Filter.tendsto_snd
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : List α
rw : Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).eraseIdx (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx (n + 1)))
⊢ Tendsto (fun (x : List α) ↦ x.eraseIdx (n + 1)) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx (n + 1)))

Tactic:
rw [tendsto_cons_iff]

Premises used: List.tendsto_cons_iff
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ p.1 :: p.2.eraseIdx n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l.eraseIdx n))

Tactic:
tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)

Premises used: Filter.Tendsto.cons, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ p.1 :: p.2.eraseIdx n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l.eraseIdx n))

Tactic:
exact tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)

Premises used: Filter.Tendsto.cons, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
⊢ Continuous[instTopologicalSpaceList, instTopologicalSpaceList] fun (l : List α) ↦ l.eraseIdx n

Tactic:
continuous_iff_continuousAt.mpr fun _a => tendsto_eraseIdx

Premises used: Iff.mpr, List.tendsto_eraseIdx, continuous_iff_continuousAt
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
⊢ Tendsto.{u_1, u_1} (α := List α) prod (𝓝 []) (𝓝 (prod []))

Tactic:
simp +contextual [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]

Premises used: Filter.tendsto_pure_left, mem_of_mem_nhds, nhds_nil
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
cons : Tendsto (fun (p : α × List α) ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)

Tactic:
simp_rw [tendsto_cons_iff, prod_cons]

Premises used: List.tendsto_cons_iff, List.prod_cons
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ ContinuousAt (Y := α) (fun (p : α × α) ↦ p.1 * p.2) (x, l.prod)

Tactic:
have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : ContinuousAt (Y := α) (fun (p : α × α) ↦ p.1 * p.2) (x, l.prod)
⊢ Tendsto (fun (p : α × α) ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))

Tactic:
rw [ContinuousAt, nhds_prod_eq] at this

Premises used: ContinuousAt, nhds_prod_eq
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : Tendsto (fun (p : α × α) ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))
⊢ Tendsto (fun (p : α × List α) ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Tactic:
this.comp (tendsto_id.prodMap ih)

Premises used: Filter.tendsto_id, Filter.Tendsto.comp, List.prod, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : Tendsto (fun (p : α × α) ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))
⊢ Tendsto (fun (p : α × List α) ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Tactic:
exact this.comp (tendsto_id.prodMap ih)

Premises used: Filter.tendsto_id, Filter.Tendsto.comp, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
l : List α
nil : Tendsto.{u_1, u_1} (α := List α) prod (𝓝 []) (𝓝 (prod []))
cons : ∀ (x : α) (l : List α) (ih : Tendsto prod (𝓝 l) (𝓝 l.prod)), Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)
⊢ Tendsto prod (𝓝 l) (𝓝 l.prod)

Tactic:
induction l with
  | nil => simp +contextual [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]
  | cons x l ih =>
    simp_rw [tendsto_cons_iff, prod_cons]
    have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
    rw [ContinuousAt, nhds_prod_eq] at this
    exact this.comp (tendsto_id.prodMap ih)

Premises used: Filter.tendsto_pure_left, ContinuousAt, mem_of_mem_nhds, nhds_nil, List.tendsto_cons_iff, List.cons, nhds_prod_eq, List.prod_cons, List.nil
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
⊢ Continuous[instTopologicalSpaceList, inst] prod

Tactic:
continuous_iff_continuousAt.mpr fun _l => tendsto_prod

Premises used: Iff.mpr, List.tendsto_prod, continuous_iff_continuousAt
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : Vector α n
rw : Tendsto (fun (x : α × Vector α n) ↦ (↑(x.1 ::ᵥ x.2) : List α)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: (↑l : List α)))
⊢ Tendsto (fun (p : α × Vector α n) ↦ p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))

Tactic:
rw [tendsto_subtype_rng, Vector.cons_val]

Premises used: List.Vector.cons_val, tendsto_subtype_rng
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun (x : α × Vector α n) ↦ (↑(x.1 ::ᵥ x.2) : List α)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: (↑l : List α)))

Tactic:
tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd)

Premises used: continuousAt_subtype_val, Filter.Tendsto.cons, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun (x : α × Vector α n) ↦ (↑(x.1 ::ᵥ x.2) : List α)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: (↑l : List α)))

Tactic:
exact tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd)

Premises used: continuousAt_subtype_val, Filter.Tendsto.cons, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
rw :
  Tendsto (fun (x : α × Vector α n) ↦ (↑(insertIdx x.1 i x.2) : List α))
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝
      (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
            ((↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl) : List α).insertIdx (↑i : ℕ) a) ⋯) :
        List α))
⊢ Tendsto (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2)
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝 (insertIdx a i (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))

Tactic:
rw [insertIdx, tendsto_subtype_rng]

Premises used: List.Vector.insertIdx, tendsto_subtype_rng
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
simp :
  Tendsto (fun (x : α × Vector α n) ↦ (↑x.2 : List α).insertIdx (↑i : ℕ) x.1)
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝 (l.insertIdx (↑i : ℕ) a))
⊢ Tendsto (fun (x : α × Vector α n) ↦ (↑(insertIdx x.1 i x.2) : List α))
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝
      (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
            ((↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl) : List α).insertIdx (↑i : ℕ) a) ⋯) :
        List α))

Tactic:
simp only [insertIdx_val]

Premises used: List.Vector.insertIdx_val
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun (x : α × Vector α n) ↦ (↑x.2 : List α).insertIdx (↑i : ℕ) x.1)
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝 (l.insertIdx (↑i : ℕ) a))

Tactic:
List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)

Premises used: continuousAt_subtype_val, List.tendsto_insertIdx, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun (x : α × Vector α n) ↦ (↑x.2 : List α).insertIdx (↑i : ℕ) x.1)
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝 (l.insertIdx (↑i : ℕ) a))

Tactic:
exact List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)

Premises used: continuousAt_subtype_val, List.tendsto_insertIdx, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x : α × Vector α n
a : α
l : Vector α n
rw : Tendsto (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))
⊢ ContinuousAt (Y := Vector α (n + 1)) (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2) (a, l)

Tactic:
rw [ContinuousAt, nhds_prod_eq]

Premises used: ContinuousAt, nhds_prod_eq
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))

Tactic:
tendsto_insertIdx

Premises used: List.Vector.tendsto_insertIdx
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))

Tactic:
exact tendsto_insertIdx

Premises used: List.Vector.tendsto_insertIdx
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
n : ℕ
i : Fin (n + 1)
f : β → α
g : β → Vector α n
hf : Continuous[inst_1, inst] f
hg : Continuous[inst_1, instTopologicalSpace n] g
⊢ Continuous[inst_1, instTopologicalSpace (n + 1)] fun (b : β) ↦ insertIdx (f b) i (g b)

Tactic:
continuous_insertIdx'.comp (hf.prodMk hg)

Premises used: List.Vector.continuous_insertIdx', Continuous.comp, List.Vector.insertIdx, Continuous.prodMk
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
rw :
  Tendsto (fun (x : Vector α (n + 1)) ↦ (↑(eraseIdx i x) : List α))
    (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl))
    (𝓝 (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1 - 1) (l.eraseIdx (↑i : ℕ)) ⋯) : List α))
⊢ ContinuousAt (eraseIdx i) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl)

Tactic:
rw [ContinuousAt, Vector.eraseIdx, tendsto_subtype_rng]

Premises used: ContinuousAt, tendsto_subtype_rng, List.Vector.eraseIdx
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
simp :
  Tendsto (fun (x : Vector α (n + 1)) ↦ (↑x : List α).eraseIdx (↑i : ℕ))
    (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl)) (𝓝 (l.eraseIdx (↑i : ℕ)))
⊢ Tendsto (fun (x : Vector α (n + 1)) ↦ (↑(eraseIdx i x) : List α))
    (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl))
    (𝓝 (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1 - 1) (l.eraseIdx (↑i : ℕ)) ⋯) : List α))

Tactic:
simp only [Vector.eraseIdx_val]

Premises used: List.Vector.eraseIdx_val
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun (x : Vector α (n + 1)) ↦ (↑x : List α).eraseIdx (↑i : ℕ))
    (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl)) (𝓝 (l.eraseIdx (↑i : ℕ)))

Tactic:
Tendsto.comp List.tendsto_eraseIdx continuousAt_subtype_val

Premises used: continuousAt_subtype_val, List.tendsto_eraseIdx, Filter.Tendsto.comp
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun (x : Vector α (n + 1)) ↦ (↑x : List α).eraseIdx (↑i : ℕ))
    (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl)) (𝓝 (l.eraseIdx (↑i : ℕ)))

Tactic:
exact Tendsto.comp List.tendsto_eraseIdx continuousAt_subtype_val

Premises used: continuousAt_subtype_val, List.tendsto_eraseIdx, Filter.Tendsto.comp
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
⊢ Continuous[instTopologicalSpace (n + 1), instTopologicalSpace (n + 1 - 1)] (eraseIdx i)

Tactic:
continuous_iff_continuousAt.mpr fun ⟨_a, _l⟩ => continuousAt_eraseIdx

Premises used: Iff.mpr, ContinuousAt, List.Vector.continuousAt_eraseIdx, _private.0.List.Vector.continuousAt_eraseIdx.match_1, List.Vector.eraseIdx, continuous_iff_continuousAt
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : IsInducing f
simp_rw :
  ∀ (h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))) (x : (↑(f ⁻¹' s) : Type u_1)),
    𝓝 x = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (comap f (𝓝 (f (↑x : α))))
⊢ IsInducing (s.restrictPreimage f)

Tactic:
simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage,
    MapsTo.coe_restrict, restrict_eq, ← @Filter.comap_comap _ _ _ _ _ f, Function.comp_apply] at h ⊢

Premises used: Set.restrictPreimage, Set.MapsTo.coe_restrict, Topology.IsInducing.of_comp_iff, Topology.isInducing_iff_nhds, Filter.comap_comap, Set.restrict_eq, Function.comp_apply, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
a : (↑(f ⁻¹' s) : Type u_1)
rw : 𝓝 a = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (𝓝 (↑a : α))
rw₁ rw₂ : 𝓝 a = 𝓝 a
⊢ 𝓝 a = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (comap f (𝓝 (f (↑a : α))))

Tactic:
rw [← h, ← IsInducing.subtypeVal.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : IsEmbedding f
⊢ IsEmbedding (s.restrictPreimage f)

Tactic:
⟨h.1.restrictPreimage s, h.2.restrictPreimage s⟩

Premises used: Topology.IsInducing.restrictPreimage, Function.Injective.restrictPreimage, Topology.IsEmbedding.injective, Topology.IsEmbedding.toIsInducing, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : IsOpenEmbedding f
⊢ IsOpenEmbedding (s.restrictPreimage f)

Tactic:
⟨h.1.restrictPreimage s,
    (s.range_restrictPreimage f).symm ▸ continuous_subtype_val.isOpen_preimage _ h.isOpen_range⟩

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, continuous_subtype_val, Set.range_restrictPreimage, Eq.rec, Topology.IsOpenEmbedding.isOpen_range, Topology.IsEmbedding.restrictPreimage, Eq.symm, Continuous.isOpen_preimage, Topology.IsOpenEmbedding.mk