awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure[inst] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
exact hc i _ hx
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst] (f i)
⊢ 𝓝[f i] x = ⊥

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx

Premises used: mem_closure_iff_nhdsWithin_neBot, Filter.not_neBot
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
neg : Tendsto g ⊥ (𝓝 (g x))
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
rw [hx]
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))

Tactic:
tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))

Tactic:
exact tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
h_cl : ∀ (i : ι), IsClosed[inst] (f i)
h_cont : ∀ (i : ι), ContinuousOn g (f i)
⊢ ContinuousOn g (⋃ (i : ι), f i)

Tactic:
hf.continuousOn_iUnion' fun i x hx ↦ h_cont i x <| (h_cl i).closure_subset hx

Premises used: IsClosed.closure_subset, LocallyFinite.continuousOn_iUnion'
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
h_cov : Eq.{u_4 + 1} (α := Set X) (⋃ (i : ι), f i) univ
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
⊢ Continuous[inst, inst_1] g

Tactic:
continuousOn_univ.1 <| h_cov ▸ hf.continuousOn_iUnion' hc

Premises used: Eq.rec, Iff.mp, continuousOn_univ, LocallyFinite.continuousOn_iUnion'
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
h_cov : Eq.{u_4 + 1} (α := Set X) (⋃ (i : ι), f i) univ
h_cl : ∀ (i : ι), IsClosed[inst] (f i)
h_cont : ∀ (i : ι), ContinuousOn g (f i)
⊢ Continuous[inst, inst_1] g

Tactic:
continuousOn_univ.1 <| h_cov ▸ hf.continuousOn_iUnion h_cl h_cont

Premises used: Eq.rec, Iff.mp, continuousOn_univ, LocallyFinite.continuousOn_iUnion
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
rcases :
  ∀ (s : Set X) (hsx : s ∈ 𝓝 x) (hsf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}),
    ∃ t ∈ 𝓝 x, Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ t).Nonempty}

Tactic:
rcases hf x with ⟨s, hsx, hsf⟩
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ t).Nonempty}

Tactic:
⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩

Premises used: Iff.mpr, Set.Finite.subset, And.intro, interior, Exists.intro, interior_mem_nhds
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}
refine :
  ∀ (i : ι)
    (hi : Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ interior s).Nonempty} i),
    Membership.mem (γ := Set ι) {i : ι | (f i ∩ s).Nonempty} i
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ t).Nonempty}

Tactic:
refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ interior s).Nonempty} i
⊢ Membership.mem (γ := Set ι) {i : ι | (f i ∩ s).Nonempty} i

Tactic:
(hi.mono isOpen_interior.closure_inter).of_closure.mono
    (inter_subset_inter_right _ interior_subset)

Premises used: Set.inter_subset_inter_right, interior_subset, IsOpen.closure_inter, Set.Mem, isOpen_interior, setOf, Set.Nonempty.mono, Set.Nonempty, Set.Nonempty.of_closure
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ interior s).Nonempty} i
⊢ Membership.mem (γ := Set ι) {i : ι | (f i ∩ s).Nonempty} i

Tactic:
exact (hi.mono isOpen_interior.closure_inter).of_closure.mono
    (inter_subset_inter_right _ interior_subset)

Premises used: Set.inter_subset_inter_right, interior_subset, IsOpen.closure_inter, isOpen_interior, Set.Nonempty.mono, Set.Nonempty.of_closure
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
h₁ :
  ∀ (x : X),
    Membership.mem (γ := Set X) (closure[inst] (⋃ (i : ι), f i)) x ↔
      Membership.mem (γ := Set X) (⋃ (i : ι), closure[inst] (f i)) x
⊢ Eq.{u_4 + 1} (α := Set X) (closure[inst] (⋃ (i : ι), f i)) (⋃ (i : ι), closure[inst] (f i))

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
x : X
⊢ Membership.mem (γ := Set X) (closure[inst] (⋃ (i : ι), f i)) x ↔
    Membership.mem (γ := Set X) (⋃ (i : ι), closure[inst] (f i)) x

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]

Premises used: Set.mem_iUnion, LocallyFinite.nhdsWithin_iUnion, mem_closure_iff_nhdsWithin_neBot, Filter.iSup_neBot
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
⊢ IsClosed[inst] (⋃ (i : ι), f i)

Tactic:
simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]

Premises used: LocallyFinite.closure_iUnion, closure_eq_iff_isClosed, IsClosed.closure_eq
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
⊢ ⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x

Tactic:
IsOpen.mem_nhds ?_ (mem_iInter₂.2 fun i => id)

Premises used: Iff.mpr, Set.mem_iInter₂, id, IsOpen.mem_nhds
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
refine : IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
⊢ ⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x

Tactic:
refine IsOpen.mem_nhds ?_ (mem_iInter₂.2 fun i => id)

Premises used: Iff.mpr, Set.mem_iInter₂, id, IsOpen.mem_nhds
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
this : IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))
rwa :
  ∀ (this : IsOpen[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))ᶜ), IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
rwa₁ :
  ∀ (this : IsOpen[inst] (⋂ (i : { i : ι // x ∉ f i }), (f (↑i : ι))ᶜ)),
    IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      IsOpen[inst] (⋂ (x_1 : ι), ⋂ (hx : x ∉ f x_1), (f (↑(Subtype.mk (p := fun (x_2 : ι) ↦ x ∉ f x_2) x_1 hx) : ι))ᶜ)),
    IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
⊢ IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this

Premises used: Set.compl_iUnion, Set.iInter_subtype, isOpen_compl_iff
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
suffices : IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))
⊢ IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by
    rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
⊢ IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))

Tactic:
(hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _

Premises used: LocallyFinite.isClosed_iUnion, Subtype.val_injective, LocallyFinite.comp_injective, Subtype.val
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
⊢ IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))

Tactic:
exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _

Premises used: LocallyFinite.isClosed_iUnion, Subtype.val_injective, LocallyFinite.comp_injective, Subtype.val
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite.{0, u_4} (X := X) fun (n : ℕ) ↦ {x : X | f (n + 1) x ≠ f n x}
choose :
  ∀ (U : (x : X) → Set X) (hUx : ∀ (x : X), U x ∈ 𝓝 x)
    (hU :
      ∀ (x : X),
        Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}),
    ∃ (F : (x : X) → π x),
      ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)

Tactic:
choose U hUx hU using hf
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
choose :
  ∀ (N : (x : X) → ℕ)
    (hN :
      ∀ (x : X),
        Membership.mem (γ := Set ℕ)
          (upperBounds {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}) (N x)),
    ∃ (F : (x : X) → π x),
      ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)

Tactic:
choose N hN using fun x => (hU x).bddAbove

Premises used: Set.Finite.bddAbove
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN :
  ∀ (x : X),
    Membership.mem (γ := Set ℕ)
      (upperBounds {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}) (N x)
⊢ ∀ (x : X), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y

Tactic:
replace hN : ∀ (x), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y :=
    fun x n hn y hy => by_contra fun hne => hn.lt.not_ge <| hN x ⟨y, hne, hy⟩
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y
⊢ ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y

Tactic:
replace hN : ∀ (x), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y :=
    fun x n hn y hy => Nat.le_induction rfl (fun k hle => (hN x _ hle _ hy).trans) n hn
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)

Tactic:
⟨fun x => f (N x + 1) x, fun x => ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
refine :
  ∀ (x : X),
    ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x),
      Eq (α := π p.2) (f p.1 p.2) ((fun (x : X) ↦ f (N x + 1) x) p.2)
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)

Tactic:
refine ⟨fun x => f (N x + 1) x, fun x => ?_⟩
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
h : ∀ a ∈ SProd.sprod (α := Set ℕ) {x_1 : ℕ | N x < x_1} (U x), Eq (α := π a.2) (f a.1 a.2) (f (N a.2 + 1) a.2)
⊢ ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x),
    Eq (α := π p.2) (f p.1 p.2) ((fun (x : X) ↦ f (N x + 1) x) p.2)

Tactic:
filter_upwards [Filter.prod_mem_prod (eventually_gt_atTop (N x)) (hUx x)]

Premises used: Filter.prod_mem_prod, Filter.eventually_gt_atTop
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ f n y = f (N x + 1) y

Tactic:
hN _ _ hn _ hy
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ f (N x + 1) y = f (max (N x + 1) (N y + 1)) y

Tactic:
(hN _ _ (le_max_left _ _) _ hy).symm

Premises used: Eq.symm, le_max_left
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ f (max (N x + 1) (N y + 1)) y = f (N y + 1) y

Tactic:
hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)

Premises used: le_max_right, mem_of_mem_nhds
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ Eq (α := π (n, y).2) (f (n, y).1 (n, y).2) (f (N (n, y).2 + 1) (n, y).2)

Tactic:
calc
    f n y = f (N x + 1) y := hN _ _ hn _ hy
    _ = f (max (N x + 1) (N y + 1)) y := (hN _ _ (le_max_left _ _) _ hy).symm
    _ = f (N y + 1) y := hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)

Premises used: le_max_right, mem_of_mem_nhds, HAdd.hAdd, Max.max, OfNat.ofNat, Eq.symm, le_max_left
-- Module: Mathlib.Topology.LocallyFinite
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite.{0, u_4} (X := X) fun (n : ℕ) ↦ {x : X | f (n + 1) x ≠ f n x}
⊢ ∃ (F : (x : X) → π x), ∀ (x : X), ∀ᶠ (n : ℕ) in atTop, ∀ᶠ (y : X) in 𝓝 x, f n y = F y

Tactic:
hf.exists_forall_eventually_eq_prod.imp fun _F hF x => (hF x).curry

Premises used: LocallyFinite.exists_forall_eventually_eq_prod, Exists.imp
-- Module: Mathlib.Topology.LocallyFinite
Goal:
α : Type u_3
X : Type u_4
inst : TopologicalSpace X
f : ℕ → X → α
hf : LocallyFinite.{0, u_4} (X := X) fun (n : ℕ) ↦ {x : X | f (n + 1) x ≠ f n x}
⊢ ∃ (F : X → α), ∀ (x : X), ∀ᶠ (n : ℕ) in atTop, f n =ᶠ[𝓝 x] F

Tactic:
hf.exists_forall_eventually_atTop_eventually_eq'

Premises used: LocallyFinite.exists_forall_eventually_atTop_eventually_eq', Filter.EventuallyEq
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : Y → X
hf : LocallyFinite f
hg : Continuous[inst_1, inst] g
⊢ LocallyFinite.{u_1, u_5} (X := Y) fun (x : ι) ↦ g ⁻¹' f x

Tactic:
fun x =>
  let ⟨s, hsx, hs⟩ := hf (g x)
  ⟨g ⁻¹' s, hg.continuousAt hsx, hs.subset fun _ ⟨y, hy⟩ => ⟨g y, hy⟩⟩

Premises used: _private.0.LocallyFinite.preimage_continuous.match_1, setOf, Set.Finite, Membership.mem, Exists, nhds, _private.0.LocallyFinite.preimage_continuous.match_2, Set.Finite.subset, LocallyFinite, Inter.inter, Continuous.continuousAt, And, Set.Nonempty, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
hf : LocallyFinite f
g : ι → Set Y
⊢ LocallyFinite (X := X × Y) fun (i : ι) ↦ f i ×ˢ g i

Tactic:
(hf.preimage_continuous continuous_fst).subset fun _ ↦ prod_subset_preimage_fst _ _

Premises used: LocallyFinite.subset, Set.prod_subset_preimage_fst, continuous_fst, LocallyFinite.preimage_continuous
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : ι → Set Y
hg : LocallyFinite g
f : ι → Set X
⊢ LocallyFinite (X := X × Y) fun (i : ι) ↦ f i ×ˢ g i

Tactic:
(hg.preimage_continuous continuous_snd).subset fun _ ↦ prod_subset_preimage_snd _ _

Premises used: LocallyFinite.subset, continuous_snd, LocallyFinite.preimage_continuous, Set.prod_subset_preimage_snd
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
e : ι' ≃ ι
h : LocallyFinite.{u_2, u_4} (ι := ι') (f ∘ (⇑e : (a : ι') → ι))
⊢ LocallyFinite f

Tactic:
simpa only [comp_def, e.apply_symm_apply] using h.comp_injective e.symm.injective

Premises used: Equiv.apply_symm_apply, Function.comp_def, Equiv.injective, Equiv.symm, LocallyFinite.comp_injective
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι ⊕ ι' → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)

Tactic:
simp only [locallyFinite_iff_smallSets, ← forall_and, ← finite_preimage_inl_and_inr,
    preimage_setOf_eq, (· ∘ ·), eventually_and]

Premises used: Filter.eventually_and, locallyFinite_iff_smallSets, Function.comp, Set.finite_preimage_inl_and_inr, Set.preimage_setOf_eq, forall_and
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → Set X
hf : LocallyFinite f
hg : LocallyFinite g
⊢ LocallyFinite (Sum.elim f g)

Tactic:
locallyFinite_sum.mpr ⟨hf, hg⟩

Premises used: Iff.mpr, locallyFinite_sum, And.intro
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : Option ι → Set X
rw :
  LocallyFinite (ι := ι)
        (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι))
          Sum.inl) ∧
      LocallyFinite (ι := PUnit.{1})
        (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι))
          Sum.inr) ↔
    LocallyFinite (f ∘ some)
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)

Tactic:
rw [← (Equiv.optionEquivSumPUnit.{0, _} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]

Premises used: locallyFinite_sum, Equiv.optionEquivSumPUnit, Equiv.locallyFinite_comp_iff, Equiv.symm
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : Option ι → Set X
simp :
  LocallyFinite (ι := ι)
      (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι)) Sum.inl) ↔
    LocallyFinite (f ∘ some)
⊢ LocallyFinite (ι := ι)
        (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι))
          Sum.inl) ∧
      LocallyFinite (ι := PUnit.{1})
        (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι))
          Sum.inr) ↔
    LocallyFinite (f ∘ some)

Tactic:
simp only [locallyFinite_of_finite, and_true]

Premises used: and_true, locallyFinite_of_finite
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite (ι := ι)
      (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι)) Sum.inl) ↔
    LocallyFinite (f ∘ some)

Tactic:
rfl
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
s : Set X
⊢ LocallyFinite (Option.elim' s f)

Tactic:
locallyFinite_option.2 hf

Premises used: Iff.mpr, locallyFinite_option
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst] (s i)
x : X
h :
  ∀ (y : X) (hy : Membership.mem (γ := Set X) (⋂ (i : ι), ⋂ (_ : x ∉ s i), (s i)ᶜ) y) ⦃i : ι⦄
    (hi : Membership.mem (γ := Set ι) {i : ι | y ∈ s i} i), Membership.mem (γ := Set ι) {i : ι | x ∈ s i} i
⊢ ∀ᶠ (y : X) in 𝓝 x, Subset.{u_1} (α := Set ι) {i : ι | y ∈ s i} {i : ι | x ∈ s i}

Tactic:
filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi

Premises used: LocallyFinite.iInter_compl_mem_nhds