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
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₂)
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 <;> [exact h₂; 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)
i : Bool
refine_2 :
  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 false then C₁ else C₂)
refine_2₁ :
  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 true then C₁ else C₂)
⊢ 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₂)

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)
refine_2 :
  Continuous[instTopologicalSpaceSubtype, dZ]
    ((bif false then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯))
⊢ 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 false then C₁ else C₂)

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- 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_2 :
  Continuous[instTopologicalSpaceSubtype, dZ]
    ((bif true then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯))
⊢ 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 true then C₁ else C₂)

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- 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[instTopologicalSpaceSubtype, dZ] g

Tactic:
hg
-- 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)
h₃ :
  (↑(bif false then C₁ else C₂) : Type u_1) = (↑C₂ : Type u_1) →
    ((bif false then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯)) =
      g
⊢ Continuous[instTopologicalSpaceSubtype, dZ]
    ((bif false then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯))

Tactic:
convert! hg
-- 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)
e_1 : (↑(bif false then C₁ else C₂) : Type u_1) = (↑C₂ : Type u_1)
h₃ :
  ∀ (x : (↑(bif false then C₁ else C₂) : Type u_1)),
    (bif false then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯))
        x =
      g x
⊢ ((bif false then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯)) =
    g

Tactic:
ext x
-- 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)
e_1 : (↑(bif false then C₁ else C₂) : Type u_1) = (↑C₂ : Type u_1)
x : (↑(bif false then C₁ else C₂) : Type u_1)
h₃ : ∀ (h : (↑x : X) ∈ C₁), f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) ⋯) = g x
⊢ (bif false then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯))
      x =
    g x

Tactic:
simp only [cond_false, restrict_apply, Subtype.coe_eta, dite_eq_right_iff]

Premises used: Set.restrict_apply, dite_eq_right_iff, Subtype.coe_eta, cond_false
-- 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)
e_1 : (↑(bif false then C₁ else C₂) : Type u_1) = (↑C₂ : Type u_1)
x : (↑(bif false then C₁ else C₂) : Type u_1)
⊢ ∀ (h : (↑x : X) ∈ C₁), f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) ⋯) = g x

Tactic:
fun hx ↦ hfg x ⟨hx, x.prop⟩

Premises used: cond, Set.Mem, Subtype.prop, And.intro, Subtype.val
-- 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)
e_1 : (↑(bif false then C₁ else C₂) : Type u_1) = (↑C₂ : Type u_1)
x : (↑(bif false then C₁ else C₂) : Type u_1)
⊢ ∀ (h : (↑x : X) ∈ C₁), f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) ⋯) = g x

Tactic:
exact fun hx ↦ hfg x ⟨hx, x.prop⟩

Premises used: Subtype.prop, And.intro, Subtype.val
-- 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_2 : Continuous[instTopologicalSpaceSubtype, dZ] fun (a : (↑C₁ : Type u_1)) ↦ f a
⊢ Continuous[instTopologicalSpaceSubtype, dZ]
    ((bif true then C₁ else C₂).restrict (π := fun (a : X) ↦ 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 ⋯))

Tactic:
simp only [cond_true, restrict_dite, Subtype.coe_eta]

Premises used: Set.restrict_dite, cond_true, Subtype.coe_eta
-- 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[instTopologicalSpaceSubtype, dZ] fun (a : (↑C₁ : Type u_1)) ↦ f a

Tactic:
hf

Premises used: cond, Set.Mem
-- 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[instTopologicalSpaceSubtype, dZ] fun (a : (↑C₁ : Type u_1)) ↦ f a

Tactic:
exact hf
-- 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 : 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₁
simp :
  Eq.{u_3 + 1} (α := Z)
    (if hi : x ∈ C₁ then (f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x hi)
      else (g : (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 hx) : Z)
⊢ Eq.{u_3 + 1} (α := Z) ((piecewise (C₁ := C₁) (C₂ := C₂) h₁ h₂ h f g hfg : (a : X) → Z) x : Z)
    ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x hx) : Z)

Tactic:
simp only [piecewise,
    coe_mk]

Premises used: LocallyConstant.piecewise, LocallyConstant.coe_mk
-- 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 : 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₁
rw rw₁ :
  Eq.{u_3 + 1} (α := Z) ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x hx) : Z)
    ((f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x hx) : Z)
⊢ Eq.{u_3 + 1} (α := Z)
    (if hi : x ∈ C₁ then (f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x hi)
      else (g : (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 hx) : Z)

Tactic:
rw [dif_pos hx]

Premises used: dif_pos
-- 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 : 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₂
simp :
  Eq.{u_3 + 1} (α := Z)
    (if hi : x ∈ C₁ then (f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x hi)
      else (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)
⊢ Eq.{u_3 + 1} (α := Z) ((piecewise (C₁ := C₁) (C₂ := C₂) h₁ h₂ h f g hfg : (a : X) → Z) x : Z)
    ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x hx) : Z)

Tactic:
simp only [piecewise,
    coe_mk]

Premises used: LocallyConstant.piecewise, LocallyConstant.coe_mk
-- 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 : 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₂
pos :
  ∀ (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)
neg :
  ∀ (h_1 : 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)
⊢ Eq.{u_3 + 1} (α := Z)
    (if hi : x ∈ C₁ then (f : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) x hi)
      else (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:
split_ifs with h