awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 : IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0})
refine_2 : IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})
⊢ IsLocallyConstant (Y := Fin 2) fun (x : X) ↦ if x ∈ U then 0 else 1

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

Premises used: Fin.forall_fin_two, Iff.mpr, And.intro, IsLocallyConstant.iff_isOpen_fiber
-- 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
⊢ IsOpen[inst_1] U

Tactic:
hU.2

Premises used: And.right
-- 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
h : preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0} = U
⊢ IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0})

Tactic:
convert! hU.2 using 1

Premises used: And.right
-- 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
h : ∀ (x : X), Membership.mem (γ := Set X) (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0}) x ↔ x ∈ U
⊢ preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0} = U

Tactic:
ext
-- 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
x : X
h : x ∉ U → False ↔ x ∈ U
⊢ Membership.mem (γ := Set X) (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0}) x ↔ x ∈ U

Tactic:
simp only [mem_singleton_iff, Fin.one_eq_zero_iff, mem_preimage, ite_eq_left_iff,
        Nat.succ_succ_ne_one]

Premises used: Fin.one_eq_zero_iff, ite_eq_left_iff, Nat.succ_succ_ne_one, Set.mem_singleton_iff, Set.mem_preimage
-- 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
x : X
h : (x ∉ U → False) → x ∈ U
h₁ : x ∈ U → x ∉ U → False
h₂ h₃ h₄ : x ∈ U → x ∈ U
h₅ h₆ h₇ h₈ : x ∈ U → x ∉ U → False
⊢ x ∉ U → False ↔ x ∈ U

Tactic:
tauto
-- 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
refine_2 : IsClosed[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ
⊢ IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})

Tactic:
rw [← isClosed_compl_iff]

Premises used: isClosed_compl_iff
-- 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
⊢ IsClosed[inst_1] U

Tactic:
hU.1

Premises used: And.left
-- 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
h : (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ = U
⊢ IsClosed[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ

Tactic:
convert! hU.1

Premises used: And.left
-- 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
h : ∀ (x : X), Membership.mem (γ := Set X) (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ x ↔ x ∈ U
⊢ (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ = U

Tactic:
ext
-- 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
x : X
⊢ Membership.mem (γ := Set X) (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ x ↔ x ∈ U

Tactic:
simp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
h :
  ∀ (x : X),
    Membership.mem (γ := Set X) (preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {0}) x ↔ x ∈ U
⊢ preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {0} = U

Tactic:
ext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
h : x ∉ U → False ↔ x ∈ U
⊢ Membership.mem (γ := Set X) (preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {0}) x ↔ x ∈ U

Tactic:
simp only [ofIsClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage,
    ite_eq_left_iff, Nat.succ_succ_ne_one]

Premises used: Fin.one_eq_zero_iff, ite_eq_left_iff, Nat.succ_succ_ne_one, LocallyConstant.coe_mk, Set.mem_singleton_iff, Set.mem_preimage, LocallyConstant.ofIsClopen
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
h : (x ∉ U → False) → x ∈ U
h₁ : x ∈ U → x ∉ U → False
h₂ h₃ h₄ : x ∈ U → x ∈ U
h₅ h₆ h₇ h₈ : x ∈ U → x ∉ U → False
⊢ x ∉ U → False ↔ x ∈ U

Tactic:
tauto
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
h :
  ∀ (x : X),
    Membership.mem (γ := Set X) (preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {1}) x ↔ x ∈ Uᶜ
⊢ preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {1} = Uᶜ

Tactic:
ext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
⊢ Membership.mem (γ := Set X) (preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {1}) x ↔ x ∈ Uᶜ

Tactic:
simp only [ofIsClopen, mem_singleton_iff, coe_mk, Fin.zero_eq_one_iff, mem_preimage,
    ite_eq_right_iff, mem_compl_iff, Nat.succ_succ_ne_one]

Premises used: Nat.succ_succ_ne_one, LocallyConstant.coe_mk, Set.mem_singleton_iff, ite_eq_right_iff, Fin.zero_eq_one_iff, Set.mem_compl_iff, Set.mem_preimage, LocallyConstant.ofIsClopen
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h :
  Eq (α := Set X) (preimage (β := Fin 2) (⇑f : (a : X) → Fin 2) {0}) (preimage (β := Fin 2) (⇑g : (a : X) → Fin 2) {0})
⊢ ∀ (x : X),
    Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2) ↔
      Eq (α := Fin 2) ((g : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2)

Tactic:
simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h

Premises used: Set.mem_singleton_iff, Set.ext_iff, Set.mem_preimage
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h :
  ∀ (x : X),
    Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2) ↔
      Eq (α := Fin 2) ((g : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2)
h₁ : ∀ (x : X), Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) ((g : (a : X) → Fin 2) x : Fin 2)
⊢ f = g

Tactic:
ext1 x
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h :
  ∀ (x : X),
    Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2) ↔
      Eq (α := Fin 2) ((g : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2)
x : X
⊢ Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) ((g : (a : X) → Fin 2) x : Fin 2)

Tactic:
Fin.fin_two_eq_of_eq_zero_iff (h x)

Premises used: Fin.fin_two_eq_of_eq_zero_iff
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h :
  ∀ (x : X),
    Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2) ↔
      Eq (α := Fin 2) ((g : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2)
x : X
⊢ Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) ((g : (a : X) → Fin 2) x : Fin 2)

Tactic:
exact Fin.fin_two_eq_of_eq_zero_iff (h x)

Premises used: Fin.fin_two_eq_of_eq_zero_iff
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : LocallyConstant X Y
⊢ Set.Finite.{u_2} (α := Y) (range.{u_2, u_1 + 1} (ι := X) (⇑f : (a : X) → Y))

Tactic:
f.isLocallyConstant.range_finite

Premises used: LocallyConstant.isLocallyConstant, IsLocallyConstant.range_finite
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : LocallyConstant X Y
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) y : Y)

Tactic:
f.isLocallyConstant.apply_eq_of_isPreconnected hs hx hy

Premises used: LocallyConstant.isLocallyConstant, 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 : LocallyConstant X Y
x y : X
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) y : Y)

Tactic:
f.isLocallyConstant.apply_eq_of_isPreconnected isPreconnected_univ trivial trivial

Premises used: trivial, LocallyConstant.isLocallyConstant, 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 : LocallyConstant X Y
x : X
⊢ f = const X ((f : (a : X) → Y) x)

Tactic:
ext fun _ => apply_eq_of_preconnectedSpace f _ _

Premises used: LocallyConstant.apply_eq_of_preconnectedSpace, LocallyConstant.ext
-- 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 : LocallyConstant X Y
inl : ∀ (x : X), ∃ (y : Y), f = const X y
inr : ∀ (hX : ¬Nonempty X), ∃ (y : Y), f = const X y
⊢ ∃ (y : Y), f = const X y

Tactic:
rcases Classical.em (Nonempty X) with (⟨⟨x⟩⟩ | hX)

Premises used: Classical.em, 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 : LocallyConstant X Y
x : X
⊢ ∃ (y : Y), f = const X y

Tactic:
⟨f x, f.eq_const x⟩

Premises used: LocallyConstant.eq_const, Exists.intro, DFunLike.coe
-- 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 : LocallyConstant X Y
x : X
⊢ ∃ (y : Y), f = const X y

Tactic:
exact ⟨f x, f.eq_const x⟩
-- 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 : LocallyConstant X Y
hX : ¬Nonempty X
⊢ ∃ (y : Y), f = const X y

Tactic:
⟨Classical.arbitrary Y, ext fun x => (hX ⟨x⟩).elim⟩

Premises used: False.elim, Nonempty.intro, Exists.intro, LocallyConstant.ext, 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 : LocallyConstant X Y
hX : ¬Nonempty X
⊢ ∃ (y : Y), f = const X y

Tactic:
exact ⟨Classical.arbitrary Y, ext fun x => (hX ⟨x⟩).elim⟩
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
f : Y → Z
g : LocallyConstant X Y
⊢ Eq (α := (a : X) → Z) (⇑(map f g) : (a : X) → Z) (f ∘ (⇑g : (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
⊢ Eq (α := (g : LocallyConstant X Y) → LocallyConstant X Y) (map id) id

Tactic:
rfl

Premises used: LocallyConstant.map, rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y₁ : Type u_5
Y₂ : Type u_6
Y₃ : Type u_7
g : Y₂ → Y₃
f : Y₁ → Y₂
⊢ Eq (α := LocallyConstant X Y₁ → LocallyConstant X Y₃) (map g ∘ map f) (map (g ∘ f))

Tactic:
rfl

Premises used: LocallyConstant.map, rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
h :
  ∀ (x : X),
    Membership.mem (γ := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g}) x ↔
      Membership.mem (γ := Set X) (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a}) x
⊢ Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
    (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})

Tactic:
ext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
x : X
⊢ Membership.mem (γ := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g}) x ↔
    Membership.mem (γ := Set X) (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a}) x

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
    (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})

Tactic:
have : (fun (x : X) (a : α) => f a x) ⁻¹' {g} = ⋂ a : α, f a ⁻¹' {g a} := by
      ext; simp [funext_iff]
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
this :
  Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
    (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
rw : IsOpen[inst_2] (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
⊢ IsOpen[inst_2] (preimage (β := α → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})

Tactic:
rw [this]
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
this :
  Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
    (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
⊢ IsOpen[inst_2] (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})

Tactic:
isOpen_iInter_of_finite fun a => (f a).isLocallyConstant _

Premises used: LocallyConstant.isLocallyConstant, isOpen_iInter_of_finite, Singleton.singleton
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
this :
  Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
    (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
⊢ IsOpen[inst_2] (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})

Tactic:
exact isOpen_iInter_of_finite fun a => (f a).isLocallyConstant _

Premises used: LocallyConstant.isLocallyConstant, isOpen_iInter_of_finite
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
α : Type u_6
β : Type u_7
inst : Finite α
inst_1 : TopologicalSpace X
f : LocallyConstant X (α → β)
⊢ unflip f.flip = f

Tactic:
rfl

Premises used: LocallyConstant.unflip, rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
α : Type u_6
β : Type u_7
inst : Finite α
inst_1 : TopologicalSpace X
f : α → LocallyConstant X β
⊢ (unflip f).flip = f

Tactic:
rfl

Premises used: LocallyConstant.flip, LocallyConstant.map, rfl
-- 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
f : C(X, Y)
g : LocallyConstant Y Z
⊢ Eq (α := (a : X) → Z) (⇑(comap f g) : (a : X) → Z)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := Y) (⇑g : (a : Y) → Z) (⇑f : (a : X) → Y))

Tactic:
rfl

Premises used: rfl
-- 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
f : C(X, Y)
g : LocallyConstant Y Z
x : X
⊢ Eq.{u_3 + 1} (α := Z) ((comap f g : (a : X) → Z) x : Z) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
⊢ Eq (α := (g : LocallyConstant X Z) → LocallyConstant X Z) (comap (ContinuousMap.id X)) id

Tactic:
rfl

Premises used: LocallyConstant.comap, rfl
-- 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
W : Type u_5
inst_2 : TopologicalSpace W
f : C(W, X)
g : C(X, Y)
⊢ Eq (α := (g : LocallyConstant Y Z) → LocallyConstant W Z) (comap (g.comp f)) (comap f ∘ comap g)

Tactic:
rfl

Premises used: LocallyConstant.comap, rfl
-- 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
W : Type u_5
inst_2 : TopologicalSpace W
f : C(W, X)
g : C(X, Y)
x : LocallyConstant Y Z
⊢ comap f (comap g x) = comap (g.comp f) x

Tactic:
rfl

Premises used: LocallyConstant.comap, ContinuousMap.comp, rfl
-- 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
f : C(X, Y)
y : Y
h : ∀ (x : X), (f : (a : X) → Y) x = y
h₁ :
  ∀ (x : LocallyConstant Y Z) (x_1 : X),
    Eq.{u_3 + 1} (α := Z) ((comap f x : (a : X) → Z) x_1 : Z)
      (((const X ((x : (a : Y) → Z) y) : LocallyConstant X Z) : (a : X) → Z) x_1 : Z)
⊢ Eq (α := (g : LocallyConstant Y Z) → LocallyConstant X Z) (comap f) fun (g : LocallyConstant Y Z) ↦
    const X ((g : (a : Y) → Z) y)

Tactic:
ext
-- 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
f : C(X, Y)
y : Y
h : ∀ (x : X), (f : (a : X) → Y) x = y
x : LocallyConstant Y Z
x_1 : X
⊢ Eq.{u_3 + 1} (α := Z) ((comap f x : (a : X) → Z) x_1 : Z)
    (((const X ((x : (a : Y) → Z) y) : LocallyConstant X Z) : (a : X) → Z) x_1 : Z)

Tactic:
simp [h]
-- 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
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
h₁ : ∀ (y : Y), Eq.{u_3 + 1} (α := Z) ((a : (a : Y) → Z) y : Z) ((b : (a : Y) → Z) y : Z)
⊢ a = b

Tactic:
ext y
-- 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
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
y : Y
h₁ : ∀ (x : X) (hx : f.toFun x = y), Eq.{u_3 + 1} (α := Z) ((a : (a : Y) → Z) y : Z) ((b : (a : Y) → Z) y : Z)
⊢ Eq.{u_3 + 1} (α := Z) ((a : (a : Y) → Z) y : Z) ((b : (a : Y) → Z) y : Z)

Tactic:
obtain ⟨x, hx⟩ := hfs y
-- 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
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
y : Y
x : X
hx : f.toFun x = y
⊢ Eq.{u_3 + 1} (α := Z) ((a : (a : Y) → Z) y : Z) ((b : (a : Y) → Z) y : Z)

Tactic:
simpa [← hx] using LocallyConstant.congr_fun h x

Premises used: LocallyConstant.congr_fun
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_5
α : Type u_6
β : Type u_7
inst : TopologicalSpace X
f : X → α
g : α → β
h : LocallyConstant X β
cond : g ∘ f = (⇑h : (a : X) → β)
inj : Function.Injective g
⊢ (⇑(desc f h cond inj) : (a : X) → α) = f

Tactic:
rfl

Premises used: 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
R : Type u_5
inst_1 : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
rw : IsOpen[inst] ((⇑f : (a : X) → R) ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)
⊢ IsOpen[inst] (U.mulIndicator (⇑f : (a : X) → R) ⁻¹' s)

Tactic:
rw [mulIndicator_preimage, Set.ite, Set.diff_eq]

Premises used: Set.ite, Set.mulIndicator_preimage, Set.diff_eq
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
R : Type u_5
inst_1 : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst] ((⇑f : (a : X) → R) ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)

Tactic:
((f.2 s).inter hU.isOpen).union ((IsLocallyConstant.const 1 s).inter hU.compl.isOpen)

Premises used: IsClopen.compl, LocallyConstant.isLocallyConstant, IsLocallyConstant.const, IsClopen.isOpen, IsOpen.union, IsOpen.inter, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
R : Type u_5
inst_1 : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst] ((⇑f : (a : X) → R) ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)

Tactic:
exact ((f.2 s).inter hU.isOpen).union ((IsLocallyConstant.const 1 s).inter hU.compl.isOpen)

Premises used: IsClopen.compl, LocallyConstant.isLocallyConstant, IsLocallyConstant.const, IsClopen.isOpen, IsOpen.union, IsOpen.inter, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
R : Type u_5
inst_1 : One R
U : Set X
f : LocallyConstant X R
a : X
hU : IsClopen U
⊢ Eq.{u_5 + 1} (α := R) ((f.mulIndicator (U := U) hU : (a : X) → R) a : R)
    (if a ∈ U then (f : (a : X) → R) a else 1 : R)

Tactic:
Set.mulIndicator_apply U f a

Premises used: Set.mulIndicator, Set.mulIndicator_apply, DFunLike.coe, ite
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
R : Type u_5
inst_1 : One R
U : Set X
f : LocallyConstant X R
a : X
hU : IsClopen U
h : a ∈ U
⊢ Eq.{u_5 + 1} (α := R) ((f.mulIndicator (U := U) hU : (a : X) → R) a : R) ((f : (a : X) → R) a : R)

Tactic:
Set.mulIndicator_of_mem h _

Premises used: Set.mulIndicator, Set.mulIndicator_of_mem, ite
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
R : Type u_5
inst_1 : One R
U : Set X
f : LocallyConstant X R
a : X
hU : IsClopen U
h : a ∉ U
⊢ Eq.{u_5 + 1} (α := R) ((f.mulIndicator (U := U) hU : (a : X) → R) a : R) (1 : R)

Tactic:
Set.mulIndicator_of_notMem h _

Premises used: Set.mulIndicator, Set.mulIndicator_of_notMem, ite