awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
f : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
g : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∈ C₁
⊢ Eq.{u_3 + 1} (α := Z) ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x h) : Z)
    ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x hx) : Z)

Tactic:
hfg x ⟨h, hx⟩

Premises used: And.intro
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
f : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
g : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∈ C₁
⊢ Eq.{u_3 + 1} (α := Z) ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x h) : Z)
    ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x hx) : Z)

Tactic:
exact hfg x ⟨h, hx⟩

Premises used: And.intro
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
f : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
g : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∉ C₁
⊢ Eq.{u_3 + 1} (α := Z) ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
    ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x hx) : Z)

Tactic:
rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
⊢ Eq (α := Set (↑C₀ : Type u_1))
    (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁ ∪ Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₂) univ

Tactic:
simpa [eq_univ_iff_forall] using h₀

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
x : X
hx₀ : x ∈ C₀
hx₁ : x ∈ C₁
hx₂ : x ∈ C₂
⊢ Eq.{u_3 + 1} (α := Z)
    ((comap { toFun := C₁.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := ⋯ } f₁ :
          (a : (↑(Subtype.val ⁻¹' C₁) : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : (↑C₀ : Type u_1)) ↦
          Membership.mem (γ := Set (↑C₀ : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) x)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₀) x hx₀) ⋯) :
      Z)
    ((comap { toFun := C₂.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := ⋯ } f₂ :
          (a : (↑(Subtype.val ⁻¹' C₂) : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : (↑C₀ : Type u_1)) ↦
          Membership.mem (γ := Set (↑C₀ : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₂) x)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₀) x hx₀) ⋯) :
      Z)

Tactic:
simpa using hf x ⟨hx₁, hx₂⟩

Premises used: And.intro
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
x : (↑C₀ : Type u_1)
hx : (↑x : X) ∈ C₁
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
rw :
  Eq.{u_3 + 1} (α := Z)
    ((comap { toFun := C₁.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := ⋯ } f₁ :
          (a : (↑(Subtype.val ⁻¹' C₁) : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : { x : X // x ∈ C₀ }) ↦
          Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) x) x hx) :
      Z)
    ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) hx) : Z)
⊢ Eq.{u_3 + 1} (α := Z)
    ((piecewise' (C₀ := C₀) (C₁ := C₁) (C₂ := C₂) h₀ h₁ h₂ f₁ f₂ hf : (a : (↑C₀ : Type u_1)) → Z) x : Z)
    ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) hx) : Z)

Tactic:
rw [piecewise', piecewise_apply_left (f := (f₁.comap
    ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
    (hx := hx)]

Premises used: Set.restrictPreimage, LocallyConstant.comap, continuous_subtype_val, ContinuousMap.mk, LocallyConstant.piecewise_apply_left, LocallyConstant.piecewise', Subtype.val, Continuous.restrictPreimage
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
x : (↑C₀ : Type u_1)
hx : (↑x : X) ∈ C₁
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
⊢ Eq.{u_3 + 1} (α := Z)
    ((comap { toFun := C₁.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := ⋯ } f₁ :
          (a : (↑(Subtype.val ⁻¹' C₁) : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : { x : X // x ∈ C₀ }) ↦
          Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) x) x hx) :
      Z)
    ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) hx) : Z)

Tactic:
rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
x : (↑C₀ : Type u_1)
hx : (↑x : X) ∈ C₂
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
rw :
  Eq.{u_3 + 1} (α := Z)
    ((comap { toFun := C₂.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := ⋯ } f₂ :
          (a : (↑(Subtype.val ⁻¹' C₂) : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : { x : X // x ∈ C₀ }) ↦
          Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₂) x) x hx) :
      Z)
    ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) (↑x : X) hx) : Z)
⊢ Eq.{u_3 + 1} (α := Z)
    ((piecewise' (C₀ := C₀) (C₁ := C₁) (C₂ := C₂) h₀ h₁ h₂ f₁ f₂ hf : (a : (↑C₀ : Type u_1)) → Z) x : Z)
    ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) (↑x : X) hx) : Z)

Tactic:
rw [piecewise', piecewise_apply_right (f := (f₁.comap
    ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
    (hx := hx)]

Premises used: Set.restrictPreimage, LocallyConstant.comap, continuous_subtype_val, ContinuousMap.mk, LocallyConstant.piecewise_apply_right, LocallyConstant.piecewise', Subtype.val, Continuous.restrictPreimage
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z) ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) : Z)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
x : (↑C₀ : Type u_1)
hx : (↑x : X) ∈ C₂
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
⊢ Eq.{u_3 + 1} (α := Z)
    ((comap { toFun := C₂.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := ⋯ } f₂ :
          (a : (↑(Subtype.val ⁻¹' C₂) : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : { x : X // x ∈ C₀ }) ↦
          Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₂) x) x hx) :
      Z)
    ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) (↑x : X) hx) : Z)

Tactic:
rfl
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
inst_1 : Finite ι
f : ι → Set X
⊢ LocallyFinite f

Tactic:
fun _ =>
  ⟨univ, univ_mem, toFinite _⟩

Premises used: Set.univ, setOf, LocallyFinite, Inter.inter, Set.toFinite, Set.Nonempty, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
⊢ Set.Finite.{u_1} (α := ι) {b : ι | x ∈ f b}

Tactic:
let ⟨_t, hxt, ht⟩ := hf x
  ht.subset fun _b hb => ⟨x, hb, mem_of_mem_nhds hxt⟩

Premises used: setOf, Set.Finite, Membership.mem, Set.Finite.subset, mem_of_mem_nhds, And.intro, Exists.intro, _private.0.LocallyFinite.point_finite.match_1
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f g : ι → Set X
hf : LocallyFinite f
hg : ∀ (i : ι), g i ⊆ f i
⊢ LocallyFinite g

Tactic:
fun a =>
  let ⟨t, ht₁, ht₂⟩ := hf a
  ⟨t, ht₁, ht₂.subset fun i hi => hi.mono <| inter_subset_inter (hg i) Subset.rfl⟩

Premises used: setOf, Set.Finite, Membership.mem, Exists, nhds, Set.Finite.subset, Set.inter_subset_inter, LocallyFinite, Set.Nonempty.mono, Inter.inter, And, Set.Nonempty, Set.Subset.rfl, And.intro, Exists.intro, _private.0.LocallyFinite.point_finite.match_1
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i : ι' | (f (g i)).Nonempty}
x : X
let :
  ∀ (t : Set X) (htx : t ∈ 𝓝 x) (htf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ t).Nonempty}),
    ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := ι') {i : ι' | ((f ∘ g) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := ι') {i : ι' | ((f ∘ g) i ∩ t).Nonempty}

Tactic:
let ⟨t, htx, htf⟩ := hf x
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i : ι' | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := ι') {i : ι' | ((f ∘ g) i ∩ t).Nonempty}

Tactic:
⟨t, htx, htf.preimage <| ?_⟩

Premises used: And.intro, Exists.intro, Set.Finite.preimage
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i : ι' | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ t).Nonempty}
refine : InjOn g (g ⁻¹' {i : ι | (f i ∩ t).Nonempty})
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := ι') {i : ι' | ((f ∘ g) i ∩ t).Nonempty}

Tactic:
refine ⟨t, htx, htf.preimage <| ?_⟩
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i : ι' | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ t).Nonempty}
⊢ InjOn g (g ⁻¹' {i : ι | (f i ∩ t).Nonempty})

Tactic:
hg.mono fun i (hi : Set.Nonempty _) => hi.left

Premises used: Set.InjOn.mono, Set.Nonempty.left
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i : ι' | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ t).Nonempty}
⊢ InjOn g (g ⁻¹' {i : ι | (f i ∩ t).Nonempty})

Tactic:
exact hg.mono fun i (hi : Set.Nonempty _) => hi.left

Premises used: Set.InjOn.mono, Set.Nonempty.left
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : Injective g
⊢ LocallyFinite (f ∘ g)

Tactic:
hf.comp_injOn hg.injOn

Premises used: Function.Injective.injOn, LocallyFinite.comp_injOn
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hg : Surjective g
hfg : LocallyFinite (f ∘ g)
⊢ LocallyFinite f

Tactic:
simpa only [comp_def, surjInv_eq hg] using hfg.comp_injective (injective_surjInv hg)

Premises used: Function.comp_def, Function.surjInv_eq, LocallyFinite.comp_injective, Function.injective_surjInv
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ LocallyFinite.{u_4, u_4} (ι := { x : Set X // x ∈ range f }) (Subtype.val (p := fun (x : Set X) ↦ x ∈ range f))

Tactic:
of_comp_surjective rangeFactorization_surjective hf

Premises used: Set.rangeFactorization_surjective, LocallyFinite.of_comp_surjective
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
⊢ LocallyFinite f ↔ ∀ (x : X), ∀ᶠ (s : Set X) in (𝓝 x).smallSets, Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}

Tactic:
forall_congr' fun _ => Iff.symm <|
    eventually_smallSets' fun _s _t hst ht =>
      ht.subset fun _i hi => hi.mono <| inter_subset_inter_right _ hst

Premises used: Set.inter_subset_inter_right, Set.Finite.subset, LocallyFinite, Set.Nonempty.mono, forall_congr', Filter.eventually_smallSets', Iff.symm
-- 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) in (𝓝 x).smallSets, Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}

Tactic:
locallyFinite_iff_smallSets.mp hf x

Premises used: locallyFinite_iff_smallSets, Iff.mp
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
ι' : Sort u_6
hf : LocallyFinite f
p : ι' → Prop
s : ι' → Set X
x : X
hb : (𝓝 x).HasBasis p s
⊢ ∃ (i : ι'), p i ∧ Set.Finite.{u_1} (α := ι) {j : ι | (f j ∩ s i).Nonempty}

Tactic:
let ⟨i, hpi, hi⟩ := hb.smallSets.eventually_iff.mp (hf.eventually_smallSets x)
  ⟨i, hpi, hi Subset.rfl⟩

Premises used: setOf, Set.Finite, Exists, Inter.inter, And, Set.Nonempty, Set.Subset.rfl, And.intro, Filter.HasBasis.smallSets, Exists.intro, Iff.mp, Filter.HasBasis.eventually_iff, _private.0.LocallyFinite.exists_mem_basis.match_1, LocallyFinite.eventually_smallSets
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
rcases :
  ∀ (U : Set X) (haU : U ∈ 𝓝 a) (hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}),
    𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a

Tactic:
rcases hf a with ⟨U, haU, hfin⟩
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a

Tactic:
le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)

Premises used: Monotone.le_map_iSup, le_antisymm, nhdsWithin_mono
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
refine : 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a

Tactic:
refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)

Premises used: Monotone.le_map_iSup, le_antisymm, nhdsWithin_mono
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
rw : 𝓝[⋃ (i : ι), f i] a = 𝓝[(⋃ (i : ι), f i) ∩ U] a
rw₁ rw₂ : 𝓝[(⋃ (i : ι), f i) ∩ U] a = 𝓝[(⋃ (i : ι), f i) ∩ U] a
⊢ 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a

Tactic:
rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]

Premises used: Set.iUnion_inter, nhdsWithin_inter_of_mem', nhdsWithin_le_nhds
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ 𝓝[⋃ (i : ι), f i ∩ U] a = 𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j : ι | (f j ∩ U).Nonempty} i), f i ∩ U] a

Tactic:
simp only [mem_setOf_eq, iUnion_nonempty_self]

Premises used: Set.mem_setOf_eq, Set.iUnion_nonempty_self
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ 𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j : ι | (f j ∩ U).Nonempty} i), f i ∩ U] a =
    ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j : ι | (f j ∩ U).Nonempty} i), 𝓝[f i ∩ U] a

Tactic:
nhdsWithin_biUnion hfin _ _

Premises used: nhdsWithin_biUnion
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ LE.le.{u_4} (α := Filter X)
    (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j : ι | (f j ∩ U).Nonempty} i), 𝓝[f i ∩ U] a)
    (⨆ (i : ι), 𝓝[f i ∩ U] a)

Tactic:
iSup₂_le_iSup _ _

Premises used: Set.Mem, setOf, iSup₂_le_iSup
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ LE.le.{u_4} (α := Filter X) (⨆ (i : ι), 𝓝[f i ∩ U] a) (⨆ (i : ι), 𝓝[f i] a)

Tactic:
iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

Premises used: Set.Mem, Set.inter_subset_left, nhdsWithin_mono, iSup_mono
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
f₁ : 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
f₂ :
  𝓝[⋃ (i : ι), f i ∩ U] a = 𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j : ι | (f j ∩ U).Nonempty} i), f i ∩ U] a
⊢ 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a

Tactic:
calc
    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_setOf_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

Premises used: nhdsWithin_biUnion, Set.inter_subset_left, iSup₂_le_iSup, nhdsWithin_mono, iSup_mono
-- 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
rw : ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
⊢ ContinuousWithinAt g (⋃ (i : ι), f i) x

Tactic:
rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]

Premises used: ContinuousWithinAt, LocallyFinite.nhdsWithin_iUnion, Filter.tendsto_iSup
-- 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 : ι
pos : ∀ (hx : x ∈ closure[inst] (f i)), Tendsto g (𝓝[f i] x) (𝓝 (g x))
neg : ∀ (hx : x ∉ closure[inst] (f i)), Tendsto g (𝓝[f i] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
by_cases hx : x ∈ closure (f i)

Premises used: closure
-- 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:
hc i _ hx

Premises used: ContinuousWithinAt