awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₜ Y
x : LocallyConstant X Z
⊢ comap (↑e : C(X, Y)) (comap (↑e.symm : C(Y, X)) x) = x

Tactic:
simp [comap_comap]

Premises used: LocallyConstant.comap_comap
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₜ Y
x : LocallyConstant Y Z
⊢ comap (↑e.symm : C(Y, X)) (comap (↑e : C(X, Y)) x) = x

Tactic:
simp [comap_comap]

Premises used: LocallyConstant.comap_comap
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
e : Y ≃ Z
x : LocallyConstant X Y
h :
  ∀ (x_1 : X),
    Eq.{u_2 + 1} (α := Y)
      ((map.{u_1, u_3, u_2} (Y := Z) (⇑e.symm : (a : Z) → Y) (map (⇑e : (a : Y) → Z) x) : (a : X) → Y) x_1 : Y)
      ((x : (a : X) → Y) x_1 : Y)
⊢ map.{u_1, u_3, u_2} (Y := Z) (⇑e.symm : (a : Z) → Y) (map (⇑e : (a : Y) → Z) x) = x

Tactic:
ext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
e : Y ≃ Z
x : LocallyConstant X Y
x_1 : X
⊢ Eq.{u_2 + 1} (α := Y)
    ((map.{u_1, u_3, u_2} (Y := Z) (⇑e.symm : (a : Z) → Y) (map (⇑e : (a : Y) → Z) x) : (a : X) → Y) x_1 : Y)
    ((x : (a : X) → Y) x_1 : Y)

Tactic:
simp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
e : Y ≃ Z
x : LocallyConstant X Z
h :
  ∀ (x_1 : X),
    Eq.{u_3 + 1} (α := Z)
      ((map.{u_1, u_2, u_3} (Y := Y) (⇑e : (a : Y) → Z) (map (⇑e.symm : (a : Z) → Y) x) : (a : X) → Z) x_1 : Z)
      ((x : (a : X) → Z) x_1 : Z)
⊢ map.{u_1, u_2, u_3} (Y := Y) (⇑e : (a : Y) → Z) (map (⇑e.symm : (a : Z) → Y) x) = x

Tactic:
ext
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
e : Y ≃ Z
x : LocallyConstant X Z
x_1 : X
⊢ Eq.{u_3 + 1} (α := Z)
    ((map.{u_1, u_2, u_3} (Y := Y) (⇑e : (a : Y) → Z) (map (⇑e.symm : (a : Z) → Y) x) : (a : X) → Z) x_1 : Z)
    ((x : (a : X) → Z) x_1 : Z)

Tactic:
simp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
inst_1 : (s : Set X) → (x : X) → Decidable (x ∈ s)
x : LocallyConstant X (Fin 2)
⊢ Eq (α := Set X)
    (preimage (β := Fin 2)
      (⇑((fun (s : TopologicalSpace.Clopens X) ↦ ofIsClopen (U := s.carrier) ⋯)
            ((fun (f : LocallyConstant X (Fin 2)) ↦
                { carrier := preimage (β := Fin 2) (⇑f : (a : X) → Fin 2) {0}, isClopen' := ⋯ :
                  TopologicalSpace.Clopens X })
              x)) :
        (a : X) → Fin 2)
      {0})
    (preimage (β := Fin 2) (⇑x : (a : X) → Fin 2) {0})

Tactic:
simp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X
inst_1 : (s : Set X) → (x : X) → Decidable (x ∈ s)
x : TopologicalSpace.Clopens X
⊢ (fun (f : LocallyConstant X (Fin 2)) ↦
        { carrier := preimage (β := Fin 2) (⇑f : (a : X) → Fin 2) {0}, isClopen' := ⋯ : TopologicalSpace.Clopens X })
      ((fun (s : TopologicalSpace.Clopens X) ↦ ofIsClopen (U := s.carrier) ⋯) x) =
    x

Tactic:
simp
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h : 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₁
dZ : TopologicalSpace Z := ⊥
⊢ DiscreteTopology Z

Tactic:
haveI : DiscreteTopology Z := discreteTopology_bot Z
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h : 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₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
obtain :
  ∀ (f : (↑C₁ : Type u_1) → Z) (hf : IsLocallyConstant f)
    (hfg :
      ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
        Eq.{u_3 + 1} (α := Z)
          (({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
                (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)),
    IsLocallyConstant.{u_1, u_3} (Y := Z) fun (i : X) ↦
      if hi : i ∈ C₁ then
        ({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
      else (g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)
⊢ IsLocallyConstant.{u_1, u_3} (Y := Z) fun (i : X) ↦
    if hi : i ∈ C₁ then (f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else (g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)

Tactic:
obtain ⟨f, hf⟩ := f
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h : C₁ ∪ C₂ = univ
g : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf : IsLocallyConstant f
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (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)
obtain :
  ∀ (g : (↑C₂ : Type u_1) → Z) (hg : IsLocallyConstant g)
    (hfg :
      ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
        Eq.{u_3 + 1} (α := Z)
          (({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
                (a : (↑C₁ : Type u_1)) → Z)
              (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
            Z)
          (({ toFun := g, isLocallyConstant := hg : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
                (a : (↑C₂ : Type u_1)) → Z)
              (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
            Z)),
    IsLocallyConstant.{u_1, u_3} (Y := Z) fun (i : X) ↦
      if hi : i ∈ C₁ then
        ({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
      else
        ({ toFun := g, isLocallyConstant := hg : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)
⊢ IsLocallyConstant.{u_1, u_3} (Y := Z) fun (i : X) ↦
    if hi : i ∈ C₁ then
      ({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
          (a : (↑C₁ : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else (g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)

Tactic:
obtain ⟨g, hg⟩ := g
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h : C₁ ∪ C₂ = univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf : IsLocallyConstant f
g : (↑C₂ : Type u_1) → Z
hg : IsLocallyConstant g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
rw :
  ∀ (hf_1 : Continuous[instTopologicalSpaceSubtype, dZ] f) (g : (↑C₂ : Type u_1) → Z) (hg : IsLocallyConstant g)
    (hg_1 : Continuous[instTopologicalSpaceSubtype, dZ] g)
    (hfg :
      ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
        Eq.{u_3 + 1} (α := Z)
          (({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
                (a : (↑C₁ : Type u_1)) → Z)
              (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
            Z)
          (({ toFun := g, isLocallyConstant := hg : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
                (a : (↑C₂ : Type u_1)) → Z)
              (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
            Z)),
    Continuous[inst, dZ] fun (i : X) ↦
      if hi : i ∈ C₁ then
        ({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
      else
        ({ toFun := g, isLocallyConstant := hg : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)
⊢ IsLocallyConstant.{u_1, u_3} (Y := Z) fun (i : X) ↦
    if hi : i ∈ C₁ then
      ({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
          (a : (↑C₁ : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else
      ({ toFun := g, isLocallyConstant := hg : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
          (a : (↑C₂ : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)

Tactic:
rw [IsLocallyConstant.iff_continuous] at hf hg ⊢

Premises used: IsLocallyConstant.iff_continuous
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h : C₁ ∪ C₂ = univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
dsimp :
  Continuous[inst, dZ] fun (i : X) ↦
    if hi : i ∈ C₁ then f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else g (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)
⊢ Continuous[inst, dZ] fun (i : X) ↦
    if hi : i ∈ C₁ then
      ({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
          (a : (↑C₁ : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else
      ({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
          (a : (↑C₂ : Type u_1)) → Z)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)

Tactic:
dsimp only [coe_mk]

Premises used: LocallyConstant.coe_mk
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h : C₁ ∪ C₂ = univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
rw :
  ∀ (h_1 : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ)
    [inst_2 : DecidablePred fun (x : X) ↦ x ∈ C₁],
    let dZ : TopologicalSpace Z := ⊥;
    ∀ (this : DiscreteTopology Z) (f : (↑C₁ : Type u_1) → Z) (hf : IsLocallyConstant f)
      (hf_2 : Continuous[instTopologicalSpaceSubtype, _] f) (g : (↑C₂ : Type u_1) → Z) (hg : IsLocallyConstant g)
      (hg_2 : Continuous[instTopologicalSpaceSubtype, _] g)
      (hfg :
        ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
          Eq.{u_3 + 1} (α := Z)
            (({ toFun := f, isLocallyConstant := hf : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
                  (a : (↑C₁ : Type u_1)) → Z)
                (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
              Z)
            (({ toFun := g, isLocallyConstant := hg : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
                  (a : (↑C₂ : Type u_1)) → Z)
                (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
              Z)),
      Continuous[inst, _] fun (i : X) ↦
        if hi : i ∈ C₁ then f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
        else g (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)
⊢ Continuous[inst, dZ] fun (i : X) ↦
    if hi : i ∈ C₁ then f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else g (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)

Tactic:
rw [Set.union_eq_iUnion] at h

Premises used: Set.union_eq_iUnion
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
h : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
⊢ Continuous[inst, dZ] fun (i : X) ↦
    if hi : i ∈ C₁ then f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else g (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)

Tactic:
(locallyFinite_of_finite _).continuous h (fun i ↦ ?_) (fun i ↦ ?_)

Premises used: locallyFinite_of_finite, LocallyFinite.continuous
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
h : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
refine_1 : ∀ (i : Bool), IsClosed[inst] (bif i then C₁ else C₂)
refine_2 :
  ∀ (i : Bool),
    ContinuousOn.{u_1, u_3} (Y := Z)
      (fun (i : X) ↦
        if hi : i ∈ C₁ then f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
        else g (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯))
      (bif i then C₁ else C₂)
⊢ Continuous[inst, dZ] fun (i : X) ↦
    if hi : i ∈ C₁ then f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) i hi)
    else g (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i ⋯)

Tactic:
refine (locallyFinite_of_finite _).continuous h (fun i ↦ ?_) (fun i ↦ ?_)

Premises used: locallyFinite_of_finite, LocallyFinite.continuous
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
h : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
i : Bool
refine_1 : IsClosed[inst] (bif false then C₁ else C₂)
refine_1₁ : IsClosed[inst] (bif true then C₁ else C₂)
⊢ IsClosed[inst] (bif i then C₁ else C₂)

Tactic:
cases i
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
h : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
⊢ IsClosed[inst] (bif false then C₁ else C₂)

Tactic:
h₂

Premises used: cond
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
h : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
⊢ IsClosed[inst] (bif false then C₁ else C₂)

Tactic:
exact h₂
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
h : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
⊢ IsClosed[inst] (bif true then C₁ else C₂)

Tactic:
h₁

Premises used: cond
-- 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₂ : Set X
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
h_1 : C₁ ∪ C₂ = univ
h : Eq.{u_1 + 1} (α := Set X) (⋃ (b : Bool), bif b then C₁ else C₂) univ
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : (↑C₁ : Type u_1) → Z
hf_1 : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : (↑C₂ : Type u_1) → Z
hg_1 : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    Eq.{u_3 + 1} (α := Z)
      (({ toFun := f, isLocallyConstant := hf_1 : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z } :
            (a : (↑C₁ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x ⋯) :
        Z)
      (({ toFun := g, isLocallyConstant := hg_1 : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z } :
            (a : (↑C₂ : Type u_1)) → Z)
          (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) :
        Z)
⊢ IsClosed[inst] (bif true then C₁ else C₂)

Tactic:
exact h₁