awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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)
⊢ 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 ⋯)
have 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 sorry) :
          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 sorry) :
          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 sorry)
Tactic: obtain ⟨g, hg⟩ := g
Cleared hypotheses: g, hfg
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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)
⊢ 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 ⋯)
have 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 sorry) :
          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 sorry) :
          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 sorry)
Tactic: rw [IsLocallyConstant.iff_continuous] at hf hg ⊢
Cleared hypotheses: g, hg, hfg
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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)
⊢ 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 ⋯)
have 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 sorry)
Tactic: dsimp only [coe_mk]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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)
⊢ 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 ⋯)
have 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 sorry) :
            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 sorry) :
            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 sorry)
Tactic: rw [Set.union_eq_iUnion] at h
Cleared hypotheses: inst_1, dZ, this, f, hf_1, hf, g, hg_1, hg, hfg
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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 ⋯)
have refine_1 : ∀ (i : Bool), IsClosed[inst] (bif i then C₁ else C₂)
Tactic: refine (locallyFinite_of_finite _).continuous h (fun i ↦ ?_) (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₂)
⊢ 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 ⋯)
have 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 sorry))
    (bif i then C₁ else C₂)
Tactic: refine (locallyFinite_of_finite _).continuous h (fun i ↦ ?_) (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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
⊢ IsClosed[inst] (bif i then C₁ else C₂)
have refine_1 : IsClosed[inst] (bif false then C₁ else C₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₂)
⊢ IsClosed[inst] (bif i then C₁ else C₂)
have refine_1₁ : IsClosed[inst] (bif true then C₁ else C₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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
⊢ IsClosed[inst] (bif i then C₁ else C₂)
have refine_1 : IsClosed[inst] (bif false then C₁ else C₂)
Tactic: cases i <;> [exact h₂; exact h₁]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₂)
⊢ IsClosed[inst] (bif i then C₁ else C₂)
have refine_1₁ : IsClosed[inst] (bif true then C₁ else C₂)
Tactic: cases i <;> [exact h₂; exact h₁]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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
⊢ 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₂)
have 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 sorry))
  (bif false then C₁ else C₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₂)
⊢ 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₂)
have 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 sorry))
  (bif true then C₁ else C₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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)
⊢ 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₂)
have 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 sorry))
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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)
⊢ 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₂)
have 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 sorry))
Tactic: rw [continuousOn_iff_continuous_restrict]