awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ) (hm : m ≤ n + k), Set.Subsingleton.{u_1} (α := ι) {j : ι | (D m j ∩ B).Nonempty}
this :
  Set.Finite.{u_1} (α := ℕ × ι)
    (⋃ (m : ℕ),
      ⋃ (_ : m ≤ n + k), ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i : ι | (D m i ∩ B).Nonempty} i), {(m, i)})
I : ℕ × ι
hI : Membership.mem (γ := Set (ℕ × ι)) {i : ℕ × ι | ((fun (ni : ℕ × ι) ↦ D ni.1 ni.2) i ∩ B).Nonempty} I
⊢ I.1 ≤ n + k

Tactic:
exact not_lt.1 fun hlt => (Hgt I.1 hlt I.2).le_bot hI.choose_spec

Premises used: Disjoint.le_bot, Exists.choose_spec, Prod.fst, not_lt, Iff.mp, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ T4Space α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
β : Type v
X : β → Type u_2
inst : Fintype β
inst_1 : (b : β) → EDist (X b)
f g : (b : β) → X b
⊢ edist f g = sup Finset.univ fun (b : β) ↦ edist (f b) (g b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
β : Type v
X : β → Type u_2
inst : Fintype β
inst_1 : (b : β) → EDist (X b)
f g : (b : β) → X b
b : β
⊢ edist (f b) (g b) ≤ edist f g

Tactic:
le_sup (f := fun b => edist (f b) (g b)) (Finset.mem_univ b)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
β : Type v
X : β → Type u_2
inst : Fintype β
inst_1 : (b : β) → EDist (X b)
f g : (b : β) → X b
d : ℝ≥0∞
⊢ (∀ (b : β), Membership.mem (γ := Finset β) Finset.univ b → edist (f b) (g b) ≤ d) ↔ ∀ (b : β), edist (f b) (g b) ≤ d

Tactic:
simp only [Finset.mem_univ, forall_const]

Premises used: Finset.mem_univ, forall_const
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : Fintype β
a b : α
⊢ (edist (α := β → α) (fun (x : β) ↦ a) fun (x : β) ↦ b) ≤ edist a b

Tactic:
edist_pi_le_iff.2 fun _ => le_rfl

Premises used: Iff.mpr, le_rfl, edist_pi_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : Fintype β
inst_2 : Nonempty β
a b : α
⊢ (edist (α := β → α) (fun (x : β) ↦ a) fun (x : β) ↦ b) = edist a b

Tactic:
Finset.sup_const univ_nonempty (edist a b)

Premises used: Finset.univ_nonempty, Finset.sup_const, EDist.edist
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
f : (b : β) → X b
⊢ ∀ (b : β), Membership.mem (γ := Finset β) Finset.univ b → edist (f b) (f b) ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
f g : (b : β) → X b
⊢ edist f g = edist g f

Tactic:
simp [edist_pi_def, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, edist_pi_def
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
simp :
  Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
    (⨅ (i : β),
      ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < i_1})
    (⨅ (ε : ℝ≥0∞),
      ⨅ (_ : 0 < ε),
        𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
⊢ Eq (α := Filter (((b : β) → X b) × ((b : β) → X b))) (𝓤 ((b : β) → X b))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | edist p.1 p.2 < ε})

Tactic:
simp only [Pi.uniformity, PseudoEMetricSpace.uniformity_edist, comap_iInf, gt_iff_lt,
      preimage_setOf_eq, comap_principal, edist_pi_def]

Premises used: Filter.comap_iInf, Set.preimage_setOf_eq, gt_iff_lt, Filter.comap_principal, edist_pi_def, PseudoEMetricSpace.uniformity_edist, Pi.uniformity
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
rw :
  Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
    (⨅ (j : ℝ≥0∞), ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
    (⨅ (ε : ℝ≥0∞),
      ⨅ (_ : 0 < ε),
        𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
⊢ Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
    (⨅ (i : β),
      ⨅ (i_1 : ℝ≥0∞), ⨅ (_ : 0 < i_1), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < i_1})
    (⨅ (ε : ℝ≥0∞),
      ⨅ (_ : 0 < ε),
        𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})

Tactic:
rw [iInf_comm]

Premises used: iInf_comm
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
e_s :
  Eq (α := ℝ≥0∞ → Filter (((b : β) → X b) × ((b : β) → X b)))
    (fun (j : ℝ≥0∞) ↦ ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
    fun (ε : ℝ≥0∞) ↦
    ⨅ (_ : 0 < ε), 𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}
⊢ Eq (α := Filter (((b : β) → X b) × ((b : β) → X b)))
    (⨅ (j : ℝ≥0∞), ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
    (⨅ (ε : ℝ≥0∞),
      ⨅ (_ : 0 < ε),
        𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})

Tactic:
congr
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
e_s :
  ∀ (ε : ℝ≥0∞),
    Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
      (⨅ (i : β), ⨅ (_ : 0 < ε), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
      (⨅ (_ : 0 < ε),
        𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
⊢ Eq (α := ℝ≥0∞ → Filter (((b : β) → X b) × ((b : β) → X b)))
    (fun (j : ℝ≥0∞) ↦ ⨅ (i : β), ⨅ (_ : 0 < j), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < j})
    fun (ε : ℝ≥0∞) ↦
    ⨅ (_ : 0 < ε), 𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
funext ε
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
e_s :
  Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (_ : 0 < ε), ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
⊢ Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (i : β), ⨅ (_ : 0 < ε), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})

Tactic:
rw [iInf_comm]

Premises used: iInf_comm
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
e_s :
  Eq (α := 0 < ε → Filter (((i : β) → X i) × ((i : β) → X i)))
    (fun (j : 0 < ε) ↦ ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    fun (x : 0 < ε) ↦
    𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}
⊢ Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (_ : 0 < ε), ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (⨅ (_ : 0 < ε),
      𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})

Tactic:
congr
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
e_s :
  ∀ (εpos : 0 < ε),
    Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
      (⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
      (𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})
⊢ Eq (α := 0 < ε → Filter (((i : β) → X i) × ((i : β) → X i)))
    (fun (j : 0 < ε) ↦ ⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    fun (x : 0 < ε) ↦
    𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
funext εpos
-- Module: Mathlib.Topology.EMetricSpace.Pi
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoEMetricSpace α
X : β → Type u_2
inst_1 : Fintype β
inst_2 : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
εpos : 0 < ε
⊢ Eq (α := Filter (((i : β) → X i) × ((i : β) → X i)))
    (⨅ (i : β), 𝓟 {a : ((i : β) → X i) × ((i : β) → X i) | edist (a.1 i) (a.2 i) < ε})
    (𝓟 {p : ((b : β) → X b) × ((b : β) → X b) | (sup Finset.univ fun (b : β) ↦ edist (p.1 b) (p.2 b)) < ε})

Tactic:
simp [setOf_forall, εpos]

Premises used: Set.setOf_forall
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
A : Set X
f : X → Y
x : X
h : ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
⊢ Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))

Tactic:
tendsto_nhds_limUnder h

Premises used: extendFrom, tendsto_nhds_limUnder
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
A : Set X
f : X → Y
x : X
y : Y
hx : x ∈ closure[inst] A
hf : Tendsto f (𝓝[A] x) (𝓝 y)
⊢ extendFrom A f x = y

Tactic:
haveI := mem_closure_iff_nhdsWithin_neBot.mp hx
  tendsto_nhds_unique (tendsto_nhds_limUnder ⟨y, hf⟩) hf

Premises used: tendsto_nhds_limUnder, Exists.intro, tendsto_nhds_unique
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
A : Set X
hf : ContinuousOn f A
⊢ ∀ x ∈ A, extendFrom A f x = f x

Tactic:
fun x x_in ↦ extendFrom_eq (subset_closure x_in) (hf x x_in)

Premises used: subset_closure, extendFrom_eq
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
set :
  let φ := extendFrom A f;
  ContinuousOn φ B
⊢ ContinuousOn (extendFrom A f) B

Tactic:
set φ := extendFrom A f

Premises used: extendFrom
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
this : ∀ V' ∈ 𝓝 (φ x), IsClosed[inst_1] V' → φ ⁻¹' V' ∈ 𝓝[B] x
⊢ ContinuousWithinAt φ B x

Tactic:
simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]

Premises used: ContinuousWithinAt, closed_nhds_basis, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
suffices : ∀ V' ∈ 𝓝 (φ x), IsClosed[inst_1] V' → φ ⁻¹' V' ∈ 𝓝[B] x
⊢ ContinuousWithinAt φ B x

Tactic:
suffices ∀ V' ∈ 𝓝 (φ x), IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x by
    simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
⊢ Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))

Tactic:
have := tendsto_extendFrom (hf x x_in)
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
this : Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
rcases :
  ∀ (V : Set X) (hV : MapsTo f (V ∩ A) V') (hxV : x ∈ V) (V_op : IsOpen[inst] V),
    ∃ V ∈ 𝓝 x, IsOpen[inst] V ∧ V ∩ A ⊆ f ⁻¹' V'
⊢ ∃ V ∈ 𝓝 x, IsOpen[inst] V ∧ V ∩ A ⊆ f ⁻¹' V'

Tactic:
rcases (nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩

Premises used: nhdsWithin_basis_open, Iff.mp, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
this : Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
V : Set X
hV : MapsTo f (V ∩ A) V'
hxV : x ∈ V
V_op : IsOpen[inst] V
⊢ ∃ V ∈ 𝓝 x, IsOpen[inst] V ∧ V ∩ A ⊆ f ⁻¹' V'

Tactic:
⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩

Premises used: And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
this : Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
V : Set X
hV : MapsTo f (V ∩ A) V'
hxV : x ∈ V
V_op : IsOpen[inst] V
⊢ ∃ V ∈ 𝓝 x, IsOpen[inst] V ∧ V ∩ A ⊆ f ⁻¹' V'

Tactic:
exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
obtain : ∀ (V : Set X) (V_in : V ∈ 𝓝 x) (V_op : IsOpen[inst] V) (hV : V ∩ A ⊆ f ⁻¹' V'), φ ⁻¹' V' ∈ 𝓝[B] x
⊢ φ ⁻¹' V' ∈ 𝓝[B] x

Tactic:
obtain ⟨V, V_in, V_op, hV⟩ : ∃ V ∈ 𝓝 x, IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V' := by
    have := tendsto_extendFrom (hf x x_in)
    rcases (nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
    exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩

Premises used: nhds
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
suffices : ∀ y ∈ V ∩ B, φ y ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x

Tactic:
suffices ∀ y ∈ V ∩ B, φ y ∈ V' from
    mem_of_superset (inter_mem_inf V_in <| mem_principal_self B) this
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
⊢ (𝓝[A] y).NeBot

Tactic:
haveI := mem_closure_iff_nhdsWithin_neBot.mp (hB hyB)
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
⊢ Tendsto f (𝓝[A] y) (𝓝 (φ y))

Tactic:
have limy : Tendsto f (𝓝[A] y) (𝓝 <| φ y) := tendsto_extendFrom (hf y hyB)
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
⊢ V ∈ 𝓝 y

Tactic:
have hVy : V ∈ 𝓝 y := IsOpen.mem_nhds V_op hyV
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
⊢ V ∩ A ∈ 𝓝[A] y

Tactic:
simpa only [inter_comm] using inter_mem_nhdsWithin A hVy

Premises used: inter_mem_nhdsWithin, Set.inter_comm
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
⊢ V ∩ A ∈ 𝓝[A] y

Tactic:
have : V ∩ A ∈ 𝓝[A] y := by simpa only [inter_comm] using inter_mem_nhdsWithin A hVy
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this_1 : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
this : V ∩ A ∈ 𝓝[A] y
⊢ φ y ∈ V'

Tactic:
V'_closed.mem_of_tendsto limy (mem_of_superset this hV)

Premises used: IsClosed.mem_of_tendsto, Filter.mem_of_superset
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst] A
hf : ∀ x ∈ B, ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst_1] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this_1 : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
this : V ∩ A ∈ 𝓝[A] y
⊢ φ y ∈ V'

Tactic:
exact V'_closed.mem_of_tendsto limy (mem_of_superset this hV)

Premises used: IsClosed.mem_of_tendsto, Filter.mem_of_superset
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
rw : ContinuousOn (extendFrom A f) univ
⊢ Continuous[inst, inst_1] (extendFrom A f)

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ∀ (x : X), Membership.mem (γ := Set X) univ x → ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)

Tactic:
simpa using hf
-- Module: Mathlib.Topology.ExtendFrom
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ (y : Y), Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) univ

Tactic:
exact continuousOn_extendFrom (fun x _ ↦ hA x) (by simpa using hf)

Premises used: continuousOn_extendFrom
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
rw : IsOpen.{u_1} (X := X) (closure ((⇑e.symm : (a : Y) → X) '' U))
⊢ IsOpen (closure U)

Tactic:
rw [e.symm.isInducing.closure_eq_preimage_closure_image, Homeomorph.isOpen_preimage]

Premises used: Homeomorph.isInducing, Homeomorph.symm, Topology.IsInducing.closure_eq_preimage_closure_image, Homeomorph.isOpen_preimage