awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
U : Set X
hU : IsOpen[inst] U
hxU : x ∈ U
eq : ∀ x' ∈ U, f x' = f x
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t

Tactic:
⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩

Premises used: Iff.mpr, Eq.rec, And.intro, Exists.intro, Eq.symm, Set.mem_preimage
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
U : Set X
hU : IsOpen[inst] U
hxU : x ∈ U
eq : ∀ x' ∈ U, f x' = f x
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t

Tactic:
exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
⊢ ∀ (a : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x), IsLocallyConstant f

Tactic:
tfae_have 5 → 1
  | h, s => by
    refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_
    rcases h x with ⟨U, hU, hxU, eq⟩
    exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
tfae_5_to_1 : ∀ (a : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x), IsLocallyConstant f
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x},
      ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y}), ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
f : X → Y
⊢ IsLocallyConstant f

Tactic:
fun _ =>
  isOpen_discrete _

Premises used: IsLocallyConstant, Set.preimage, isOpen_discrete
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
y : Y
⊢ IsOpen[inst] {x : X | f x = y}

Tactic:
hf {y}

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Singleton.singleton
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
y : Y
⊢ IsClosed[inst] {x : X | f x = y}

Tactic:
⟨hf {y}ᶜ⟩

Premises used: Compl.compl, IsClosed.mk, Singleton.singleton
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
y : Y
⊢ IsClopen.{u_1} (X := X) {x : X | f x = y}

Tactic:
⟨isClosed_fiber hf _, isOpen_fiber hf _⟩

Premises used: IsLocallyConstant.isClosed_fiber, IsLocallyConstant.isOpen_fiber, And.intro, IsClopen
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyConstant f ↔ ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
(IsLocallyConstant.tfae f).out 0 4

Premises used: IsLocallyConstant.tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyConstant f ↔ ∀ (x : X), ∀ᶠ (y : X) in 𝓝 x, f y = f x

Tactic:
(IsLocallyConstant.tfae f).out 0 1

Premises used: IsLocallyConstant.tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
x : X
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
(iff_exists_open f).1 hf x

Premises used: IsLocallyConstant.iff_exists_open, Iff.mp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
x : X
⊢ ∀ᶠ (y : X) in 𝓝 x, f y = f x

Tactic:
(iff_eventually_eq f).1 hf x

Premises used: IsLocallyConstant.iff_eventually_eq, Iff.mp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyConstant f ↔ ∀ (x : X), IsOpen[inst] (f ⁻¹' {f x})

Tactic:
(IsLocallyConstant.tfae f).out 0 2

Premises used: IsLocallyConstant.tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ IsLocallyConstant f ↔ ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})

Tactic:
(IsLocallyConstant.tfae f).out 0 3

Premises used: IsLocallyConstant.tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocallyConstant f
⊢ Continuous[inst, inst_1] f

Tactic:
⟨fun _ _ => hf _⟩

Premises used: Continuous.mk
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
x : TopologicalSpace Y
inst_1 : DiscreteTopology Y
f : X → Y
⊢ IsLocallyConstant f ↔ Continuous[inst, x] f

Tactic:
⟨IsLocallyConstant.continuous, fun h s => h.isOpen_preimage s (isOpen_discrete _)⟩

Premises used: isOpen_discrete, Iff.intro, IsLocallyConstant.continuous, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x y : X), f x = f y
⊢ IsLocallyConstant f

Tactic:
(iff_eventually_eq f).2 fun _ => Eventually.of_forall fun _ => h _ _

Premises used: Iff.mpr, IsLocallyConstant.iff_eventually_eq, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
⊢ IsLocallyConstant (Function.const X y)

Tactic:
of_constant _ fun _ _ => rfl

Premises used: IsLocallyConstant.of_constant, rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
rw : IsOpen[inst] (f ⁻¹' g ⁻¹' s)
⊢ IsOpen[inst] (g ∘ f ⁻¹' s)

Tactic:
rw [Set.preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen[inst] (f ⁻¹' g ⁻¹' s)

Tactic:
hf _
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen[inst] (f ⁻¹' g ⁻¹' s)

Tactic:
exact hf _
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
Y' : Type u_5
f : X → Y
f' : X → Y'
hf : IsLocallyConstant f
hf' : IsLocallyConstant f'
⊢ IsLocallyConstant (Y := Y × Y') fun (x : X) ↦ (f x, f' x)

Tactic:
(iff_eventually_eq _).2 fun x =>
    (hf.eventually_eq x).mp <| (hf'.eventually_eq x).mono fun _ hf' hf => Prod.ext hf hf'

Premises used: Iff.mpr, IsLocallyConstant.iff_eventually_eq, IsLocallyConstant.eventually_eq, Filter.Eventually.mono, Filter.Eventually.mp, Prod.ext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y₁ : Type u_5
Y₂ : Type u_6
Z : Type u_7
f : X → Y₁
g : X → Y₂
hf : IsLocallyConstant f
hg : IsLocallyConstant g
h : Y₁ → Y₂ → Z
⊢ IsLocallyConstant.{u_1, u_7} (Y := Z) fun (x : X) ↦ h (f x) (g x)

Tactic:
(hf.prodMk hg).comp fun x : Y₁ × Y₂ => h x.1 x.2

Premises used: Prod.fst, IsLocallyConstant.comp, IsLocallyConstant.prodMk, Prod.snd
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous[inst, inst_1] f
s : Set Z
rw : IsOpen[inst] (f ⁻¹' g ⁻¹' s)
⊢ IsOpen[inst] (g ∘ f ⁻¹' s)

Tactic:
rw [Set.preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous[inst, inst_1] f
s : Set Z
⊢ IsOpen[inst] (f ⁻¹' g ⁻¹' s)

Tactic:
hf.isOpen_preimage _ (hg _)

Premises used: Continuous.isOpen_preimage
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous[inst, inst_1] f
s : Set Z
⊢ IsOpen[inst] (f ⁻¹' g ⁻¹' s)

Tactic:
exact hf.isOpen_preimage _ (hg _)

Premises used: Continuous.isOpen_preimage
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
suffices : x ∉ Uᶜ
⊢ f x = f y

Tactic:
suffices x ∉ Uᶜ from Classical.not_not.1 this
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
specialize : s ⊆ U ∪ Uᶜ
specialize₁ : ∀ (hs : (s ∩ (U ∩ Uᶜ)).Nonempty), False
⊢ False

Tactic:
specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩

Premises used: Compl.compl, And.intro, Exists.intro, Singleton.singleton, rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ s ⊆ U ∪ Uᶜ

Tactic:
simp only [union_compl_self, subset_univ]

Premises used: Set.subset_univ, Set.union_compl_self
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
hs : (s ∩ (U ∩ Uᶜ)).Nonempty
⊢ False

Tactic:
simp only [inter_empty, Set.not_nonempty_empty, inter_compl_self] at hs

Premises used: Set.not_nonempty_empty, Set.inter_compl_self, Set.inter_empty
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
f : X → Y
hf : IsLocallyConstant f
x y : X
⊢ f x = f y

Tactic:
hf.apply_eq_of_isPreconnected isPreconnected_univ trivial trivial

Premises used: trivial, PreconnectedSpace.isPreconnected_univ, IsLocallyConstant.apply_eq_of_isPreconnected
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
f : X → Y
hf : IsLocallyConstant f
x : X
⊢ f = Function.const X (f x)

Tactic:
funext fun y => hf.apply_eq_of_preconnectedSpace y x

Premises used: IsLocallyConstant.apply_eq_of_preconnectedSpace, funext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
inl : ∀ (h : IsEmpty X), ∃ (y : Y), f = Function.const X y
inr : ∀ (h : Nonempty X), ∃ (y : Y), f = Function.const X y
⊢ ∃ (y : Y), f = Function.const X y

Tactic:
rcases isEmpty_or_nonempty X with h | h

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ (y : Y), f = Function.const X y

Tactic:
⟨Classical.arbitrary Y, funext <| h.elim⟩

Premises used: IsEmpty.elim, funext, Exists.intro, Classical.arbitrary
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ (y : Y), f = Function.const X y

Tactic:
exact ⟨Classical.arbitrary Y, funext <| h.elim⟩
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ (y : Y), f = Function.const X y

Tactic:
⟨f (Classical.arbitrary X), hf.eq_const _⟩

Premises used: Exists.intro, Classical.arbitrary, IsLocallyConstant.eq_const
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ (y : Y), f = Function.const X y

Tactic:
exact ⟨f (Classical.arbitrary X), hf.eq_const _⟩
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
f : X → Y
⊢ IsLocallyConstant f ↔ ∀ (x y : X), f x = f y

Tactic:
⟨fun h _ _ => h.apply_eq_of_isPreconnected isPreconnected_univ trivial trivial, of_constant _⟩

Premises used: trivial, Iff.intro, PreconnectedSpace.isPreconnected_univ, IsLocallyConstant.of_constant, IsLocallyConstant.apply_eq_of_isPreconnected
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ DiscreteTopology Y

Tactic:
haveI := discreteTopology_bot Y
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this_1 : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ (range f).Finite

Tactic:
(isCompact_range hf.continuous).finite_of_discrete

Premises used: isCompact_range, IsCompact.finite_of_discrete, IsLocallyConstant.continuous
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this_1 : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ (range f).Finite

Tactic:
exact (isCompact_range hf.continuous).finite_of_discrete

Premises used: isCompact_range, IsCompact.finite_of_discrete, IsLocallyConstant.continuous
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : One Y
⊢ IsLocallyConstant.{u_1, u_2} (X := X) (Y := Y) 1

Tactic:
IsLocallyConstant.const 1

Premises used: IsLocallyConstant.const, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Inv Y
f : X → Y
hf : IsLocallyConstant f
⊢ IsLocallyConstant f⁻¹

Tactic:
hf.comp fun x => x⁻¹

Premises used: Inv.inv, IsLocallyConstant.comp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Mul Y
f g : X → Y
hf : IsLocallyConstant f
hg : IsLocallyConstant g
⊢ IsLocallyConstant (f * g)

Tactic:
hf.comp₂ hg (· * ·)

Premises used: HMul.hMul, IsLocallyConstant.comp₂
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Div Y
f g : X → Y
hf : IsLocallyConstant f
hg : IsLocallyConstant g
⊢ IsLocallyConstant (f / g)

Tactic:
hf.comp₂ hg (· / ·)

Premises used: HDiv.hDiv, IsLocallyConstant.comp₂
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
rw : IsOpen[inst] ((fun (x : X) ↦ g (f x)) ⁻¹' g '' s)
⊢ IsOpen[inst] (f ⁻¹' s)

Tactic:
rw [← preimage_image_eq s inj, preimage_preimage]

Premises used: Set.preimage_preimage, Set.preimage_image_eq
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen[inst] ((fun (x : X) ↦ g (f x)) ⁻¹' g '' s)

Tactic:
h (g '' s)

Premises used: Set.image
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen[inst] ((fun (x : X) ↦ g (f x)) ⁻¹' g '' s)

Tactic:
exact h (g '' s)

Premises used: Set.image
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : LocallyConnectedSpace X
f : X → Y
h : ∀ (x y : X), y ∈ connectedComponent x → f y = f x
⊢ IsLocallyConstant f

Tactic:
(iff_exists_open _).2 fun x =>
    ⟨connectedComponent x, isOpen_connectedComponent, mem_connectedComponent, h x⟩

Premises used: Iff.mpr, IsLocallyConstant.iff_exists_open, mem_connectedComponent, connectedComponent, isOpen_connectedComponent, And.intro, Exists.intro
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : LocallyConnectedSpace X
f : X → Y
h : ∀ (U : Set X), IsConnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x
⊢ IsLocallyConstant f

Tactic:
of_constant_on_connected_components fun x =>
    h (connectedComponent x) isConnected_connectedComponent isClopen_connectedComponent x
      mem_connectedComponent

Premises used: isConnected_connectedComponent, mem_connectedComponent, connectedComponent, isClopen_connectedComponent, IsLocallyConstant.of_constant_on_connected_components
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : LocallyConnectedSpace X
f : X → Y
h : ∀ (U : Set X), IsPreconnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x
⊢ IsLocallyConstant f

Tactic:
of_constant_on_connected_clopens fun U hU ↦ h U hU.isPreconnected

Premises used: IsLocallyConstant.of_constant_on_connected_clopens, IsConnected.isPreconnected
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
toFun : X → Y
isLocallyConstant : IsLocallyConstant toFun
toFun_1 : X → Y
isLocallyConstant_1 : IsLocallyConstant toFun_1
h :
  { toFun := toFun, isLocallyConstant := isLocallyConstant : LocallyConstant X Y }.toFun =
    { toFun := toFun_1, isLocallyConstant := isLocallyConstant_1 : LocallyConstant X Y }.toFun
⊢ { toFun := toFun, isLocallyConstant := isLocallyConstant : LocallyConstant X Y } =
    { toFun := toFun_1, isLocallyConstant := isLocallyConstant_1 }

Tactic:
congr
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : LocallyConstant X Y
⊢ f.toFun = (⇑f : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : IsLocallyConstant f
⊢ (⇑{ toFun := f, isLocallyConstant := h : LocallyConstant X Y } : (a : X) → Y) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f g : LocallyConstant X Y
h : f = g
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : LocallyConstant X Y
x y : X
h : x = y
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) y : Y)

Tactic:
DFunLike.congr_arg f h

Premises used: DFunLike.congr_arg
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
⊢ Function.Injective (α := LocallyConstant X Y) (β := X → Y) (DFunLike.coe (β := fun (x : X) ↦ Y))

Tactic:
fun _ _ =>
  DFunLike.ext'

Premises used: Function.Injective, DFunLike.ext'
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f g : LocallyConstant X Y
⊢ Eq (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) ↔ f = g

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, LocallyConstant.coe_injective
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f g : LocallyConstant X Y
h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : LocallyConstant X Y
⊢ Continuous[inst, inst_1] (⇑f : (a : X) → Y)

Tactic:
f.isLocallyConstant.continuous

Premises used: LocallyConstant.isLocallyConstant, IsLocallyConstant.continuous
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : LocallyConstant X Y
⊢ Eq (α := (a : X) → Y) (⇑(↑f : C(X, Y)) : (a : X) → Y) (⇑f : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Function.Injective (α := LocallyConstant X Y) (β := C(X, Y)) toContinuousMap

Tactic:
fun _ _ h =>
  ext (ContinuousMap.congr_fun h)

Premises used: ContinuousMap.congr_fun, LocallyConstant.ext, Function.Injective
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
y : Y
⊢ (⇑(const X y) : (a : X) → Y) = Function.const X y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsLocallyConstant (Y := Fin 2) fun (x : X) ↦ if x ∈ U then 0 else 1

Tactic:
IsLocallyConstant.iff_isOpen_fiber.2 <| Fin.forall_fin_two.2 ⟨?_, ?_⟩

Premises used: Fin.forall_fin_two, Iff.mpr, And.intro, IsLocallyConstant.iff_isOpen_fiber