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_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]
    ((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 ⋯))
have 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 sorry)) =
    g
Tactic: convert! hg
-- 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)
e_1 : (↑(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
have 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 sorry))
      x =
    g x
Tactic: ext x
-- 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)
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)
⊢ (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
have h₃ : ∀ (h : (↑x : X) ∈ C₁), f (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) sorry) = g x
Tactic: simp only [cond_false, restrict_apply, Subtype.coe_eta, dite_eq_right_iff]
-- 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[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 ⋯))
have refine_2 : Continuous[instTopologicalSpaceSubtype, dZ] fun (a : (↑C₁ : Type u_1)) ↦ f a
Tactic: simp only [cond_true, restrict_dite, Subtype.coe_eta]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₁
⊢ 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)
have 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 sorry) :
    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]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₁
⊢ 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)
have 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)
Tactic: rw [dif_pos hx]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₂
⊢ 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)
have 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 sorry) :
    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]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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₂
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
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)
⊢ 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)
have 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 sorry) : Z)
    ((g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x hx) : Z)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (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)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
x : (↑C₀ : Type u_1)
hx : (↑x : X) ∈ C₁
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
⊢ Eq.{u_3 + 1} (α := Z)
    ((piecewise' (C₀ := C₀) (C₁ := C₁) (C₂ := C₂) h₀ h₁ h₂ f₁ f₂ hf : (a : (↑C₀ : Type u_1)) → Z) x : Z)
    ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) hx) : Z)
have rw : Eq.{u_3 + 1} (α := Z)
  ((comap { toFun := C₁.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := sorry } f₁ :
        (a : (↑(Subtype.val ⁻¹' C₁) : Type u_1)) → Z)
      (Subtype.mk (p := fun (x : { x : X // x ∈ C₀ }) ↦
        Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) x) x hx) :
    Z)
  ((f₁ : (a : (↑C₁ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₁) (↑x : X) hx) : Z)
Tactic: rw [piecewise', piecewise_apply_left (f := (f₁.comap
    ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
    (hx := hx)]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Z : Type u_3
inst : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst] C₁
h₂ : IsClosed[inst] C₂
f₁ : LocallyConstant.{u_1, u_3} (↑C₁ : Type u_1) Z
f₂ : LocallyConstant.{u_1, u_3} (↑C₂ : Type u_1) Z
inst_1 : DecidablePred fun (x : X) ↦ x ∈ C₁
hf :
  ∀ (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)
      ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) x ⋯) : Z)
x : (↑C₀ : Type u_1)
hx : (↑x : X) ∈ C₂
this : (j : (↑C₀ : Type u_1)) →
  Decidable (Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₁) j) :=
  fun (j : (↑C₀ : Type u_1)) ↦ decidable_of_iff ((↑j : X) ∈ C₁) ⋯
⊢ Eq.{u_3 + 1} (α := Z)
    ((piecewise' (C₀ := C₀) (C₁ := C₁) (C₂ := C₂) h₀ h₁ h₂ f₁ f₂ hf : (a : (↑C₀ : Type u_1)) → Z) x : Z)
    ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) (↑x : X) hx) : Z)
have rw : Eq.{u_3 + 1} (α := Z)
  ((comap { toFun := C₂.restrictPreimage (Subtype.val (p := fun (x : X) ↦ x ∈ C₀)), continuous_toFun := sorry } f₂ :
        (a : (↑(Subtype.val ⁻¹' C₂) : Type u_1)) → Z)
      (Subtype.mk (p := fun (x : { x : X // x ∈ C₀ }) ↦
        Membership.mem (γ := Set { x : X // x ∈ C₀ }) (Subtype.val (p := fun (x : X) ↦ x ∈ C₀) ⁻¹' C₂) x) x hx) :
    Z)
  ((f₂ : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) (↑x : X) hx) : Z)
Tactic: rw [piecewise', piecewise_apply_right (f := (f₁.comap
    ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
    (hx := hx)]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i : ι' | (f (g i)).Nonempty}
x : X
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := ι') {i : ι' | ((f ∘ g) i ∩ t).Nonempty}
have let : ∀ (t : Set X) (htx : t ∈ 𝓝 x) (htf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ t).Nonempty}),
  ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := ι') {i : ι' | ((f ∘ g) i ∩ t).Nonempty}
Tactic: let ⟨t, htx, htf⟩ := hf x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i : ι' | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := ι') {i : ι' | ((f ∘ g) i ∩ t).Nonempty}
have refine : InjOn g (g ⁻¹' {i : ι | (f i ∩ t).Nonempty})
Tactic: refine ⟨t, htx, htf.preimage <| ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
have rcases : ∀ (U : Set X) (haU : U ∈ 𝓝 a) (hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}),
  𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
Tactic: rcases hf a with ⟨U, haU, hfin⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
have refine : 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
Tactic: refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
have rw : 𝓝[⋃ (i : ι), f i] a = 𝓝[(⋃ (i : ι), f i) ∩ U] a
Tactic: rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
rw : 𝓝[⋃ (i : ι), f i] a = 𝓝[(⋃ (i : ι), f i) ∩ U] a
⊢ 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
have rw₁ : 𝓝[(⋃ (i : ι), f i) ∩ U] a = 𝓝[(⋃ (i : ι), f i) ∩ U] a
Tactic: rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
⊢ 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
have f₁ : 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
Tactic: calc
    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_setOf_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ U).Nonempty}
f₁ : 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
⊢ 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
have f₂ : 𝓝[⋃ (i : ι), f i ∩ U] a = 𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) {j : ι | (f j ∩ U).Nonempty} i), f i ∩ U] a
Tactic: calc
    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_setOf_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ (i : ι), f i) x
have rw : ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
Tactic: rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
have pos : ∀ (hx : x ∈ closure[inst] (f i)), Tendsto g (𝓝[f i] x) (𝓝 (g x))
Tactic: by_cases hx : x ∈ closure (f i)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
pos : ∀ (hx : x ∈ closure[inst] (f i)), Tendsto g (𝓝[f i] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
have neg : ∀ (hx : x ∉ closure[inst] (f i)), Tendsto g (𝓝[f i] x) (𝓝 (g x))
Tactic: by_cases hx : x ∈ closure (f i)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (hypothesis)
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
have hx₁ : 𝓝[f i] x = ⊥
Tactic: rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
have neg : Tendsto g ⊥ (𝓝 (g x))
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ t).Nonempty}
have rcases : ∀ (s : Set X) (hsx : s ∈ 𝓝 x) (hsf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}),
  ∃ t ∈ 𝓝 x, Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ t).Nonempty}
Tactic: rcases hf x with ⟨s, hsx, hsf⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite.{u_1} (α := ι) {i : ι | (f i ∩ s).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ t).Nonempty}
have refine : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ closure[inst] (f i)) i ∩ interior s).Nonempty} i),
  Membership.mem (γ := Set ι) {i : ι | (f i ∩ s).Nonempty} i
Tactic: refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
⊢ Eq.{u_4 + 1} (α := Set X) (closure[inst] (⋃ (i : ι), f i)) (⋃ (i : ι), closure[inst] (f i))
have h₁ : ∀ (x : X),
  Membership.mem (γ := Set X) (closure[inst] (⋃ (i : ι), f i)) x ↔
    Membership.mem (γ := Set X) (⋃ (i : ι), closure[inst] (f i)) x
Tactic: ext x