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
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
have rcases : ∀ (U : Set X) (eq : U ⊆ {x_1 : X | (fun (x' : X) ↦ f x' = f x) x_1}) (hU : IsOpen[inst] U) (hx : x ∈ U),
  ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
Tactic: rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x},
      ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y}), ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
have tfae_2_to_5 : ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
Tactic: tfae_have 2 → 5
  | h, x => by
    rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩
    exact ⟨U, hU, hx, eq⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
⊢ IsOpen[inst] (f ⁻¹' s)
have refine : ∀ (x : X) (hx : x ∈ f ⁻¹' s), ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t
Tactic: refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t
have rcases : ∀ (U : Set X) (hU : IsOpen[inst] U) (hxU : x ∈ U) (eq : ∀ x' ∈ U, f x' = f x), ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t
Tactic: rcases h x with ⟨U, hU, hxU, eq⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x},
      ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y}), ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
have tfae_5_to_1 : ∀ (a : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x), IsLocallyConstant f
Tactic: tfae_have 5 → 1
  | h, s => by
    refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_
    rcases h x with ⟨U, hU, hxU, eq⟩
    exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen[inst] (g ∘ f ⁻¹' s)
have rw : IsOpen[inst] (f ⁻¹' g ⁻¹' s)
Tactic: rw [Set.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous[inst, inst_1] f
s : Set Z
⊢ IsOpen[inst] (g ∘ f ⁻¹' s)
have rw : IsOpen[inst] (f ⁻¹' g ⁻¹' s)
Tactic: rw [Set.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ f x = f y
have suffices : x ∉ Uᶜ
Tactic: suffices x ∉ Uᶜ from Classical.not_not.1 this
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ False
have specialize : s ⊆ U ∪ Uᶜ
Tactic: specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
specialize : s ⊆ U ∪ Uᶜ
⊢ False
have specialize₁ : ∀ (hs : (s ∩ (U ∩ Uᶜ)).Nonempty), False
Tactic: specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
⊢ ∃ (y : Y), f = Function.const X y
have inl : ∀ (h : IsEmpty X), ∃ (y : Y), f = Function.const X y
Tactic: rcases isEmpty_or_nonempty X with h | h
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
inl : ∀ (h : IsEmpty X), ∃ (y : Y), f = Function.const X y
⊢ ∃ (y : Y), f = Function.const X y
have inr : ∀ (h : Nonempty X), ∃ (y : Y), f = Function.const X y
Tactic: rcases isEmpty_or_nonempty X with h | h
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ (range f).Finite
have this₁ : DiscreteTopology Y
Tactic: haveI := discreteTopology_bot Y
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen[inst] (f ⁻¹' s)
have rw : IsOpen[inst] ((fun (x : X) ↦ g (f x)) ⁻¹' g '' s)
Tactic: rw [← preimage_image_eq s inj, preimage_preimage]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsLocallyConstant (Y := Fin 2) fun (x : X) ↦ if x ∈ U then 0 else 1
have refine_1 : IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0})
Tactic: refine IsLocallyConstant.iff_isOpen_fiber.2 <| Fin.forall_fin_two.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
refine_1 : IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0})
⊢ IsLocallyConstant (Y := Fin 2) fun (x : X) ↦ if x ∈ U then 0 else 1
have refine_2 : IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})
Tactic: refine IsLocallyConstant.iff_isOpen_fiber.2 <| Fin.forall_fin_two.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0})
have h : preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0} = U
Tactic: convert! hU.2 using 1
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0} = U
have h : ∀ (x : X), Membership.mem (γ := Set X) (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0}) x ↔ x ∈ U
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
⊢ Membership.mem (γ := Set X) (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {0}) x ↔ x ∈ U
have h : x ∉ U → False ↔ x ∈ U
Tactic: simp only [mem_singleton_iff, Fin.one_eq_zero_iff, mem_preimage, ite_eq_left_iff,
        Nat.succ_succ_ne_one]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
⊢ x ∉ U → False ↔ x ∈ U
have h : (x ∉ U → False) → x ∈ U
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
h : (x ∉ U → False) → x ∈ U
⊢ x ∉ U → False ↔ x ∈ U
have h₁ : x ∈ U → x ∉ U → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
h : (x ∉ U → False) → x ∈ U
h₁ : x ∈ U → x ∉ U → False
⊢ x ∉ U → False ↔ x ∈ U
have h₂ : x ∈ U → x ∈ U
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsOpen[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})
have refine_2 : IsClosed[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ
Tactic: rw [← isClosed_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsClosed[inst_1] (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ
have h : (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ = U
Tactic: convert! hU.1
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
inst_1 : TopologicalSpace X
U : Set X
inst_2 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ = U
have h : ∀ (x : X), Membership.mem (γ := Set X) (preimage (β := Fin 2) (fun (x : X) ↦ if x ∈ U then 0 else 1) {1})ᶜ x ↔ x ∈ U
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {0} = U
have h : ∀ (x : X),
  Membership.mem (γ := Set X) (preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {0}) x ↔ x ∈ U
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
⊢ Membership.mem (γ := Set X) (preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {0}) x ↔ x ∈ U
have h : x ∉ U → False ↔ x ∈ U
Tactic: simp only [ofIsClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage,
    ite_eq_left_iff, Nat.succ_succ_ne_one]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
⊢ x ∉ U → False ↔ x ∈ U
have h : (x ∉ U → False) → x ∈ U
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
h : (x ∉ U → False) → x ∈ U
⊢ x ∉ U → False ↔ x ∈ U
have h₁ : x ∈ U → x ∉ U → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x : X
h : (x ∉ U → False) → x ∈ U
h₁ : x ∈ U → x ∉ U → False
⊢ x ∉ U → False ↔ x ∈ U
have h₂ : x ∈ U → x ∈ U
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_5
inst : TopologicalSpace X
U : Set X
inst_1 : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {1} = Uᶜ
have h : ∀ (x : X),
  Membership.mem (γ := Set X) (preimage (β := Fin 2) (⇑(ofIsClopen (U := U) hU) : (a : X) → Fin 2) {1}) x ↔ x ∈ Uᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X : Type u_5
inst : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h :
  Eq (α := Set X) (preimage (β := Fin 2) (⇑f : (a : X) → Fin 2) {0}) (preimage (β := Fin 2) (⇑g : (a : X) → Fin 2) {0})
⊢ f = g
have h₁ : ∀ (x : X),
  Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2) ↔
    Eq (α := Fin 2) ((g : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2)
Tactic: simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_5
inst : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h :
  ∀ (x : X),
    Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2) ↔
      Eq (α := Fin 2) ((g : (a : X) → Fin 2) x : Fin 2) (0 : Fin 2)
⊢ f = g
have h₁ : ∀ (x : X), Eq (α := Fin 2) ((f : (a : X) → Fin 2) x : Fin 2) ((g : (a : X) → Fin 2) x : Fin 2)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : LocallyConstant X Y
⊢ ∃ (y : Y), f = const X y
have inl : ∀ (x : X), ∃ (y : Y), f = const X y
Tactic: rcases Classical.em (Nonempty X) with (⟨⟨x⟩⟩ | hX)
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nonempty Y
f : LocallyConstant X Y
inl : ∀ (x : X), ∃ (y : Y), f = const X y
⊢ ∃ (y : Y), f = const X y
have inr : ∀ (hX : ¬Nonempty X), ∃ (y : Y), f = const X y
Tactic: rcases Classical.em (Nonempty X) with (⟨⟨x⟩⟩ | hX)
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
    (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
have h : ∀ (x : X),
  Membership.mem (γ := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g}) x ↔
    Membership.mem (γ := Set X) (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ IsOpen[inst_2] (preimage (β := α → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
have this : Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
  (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
Tactic: have : (fun (x : X) (a : α) => f a x) ⁻¹' {g} = ⋂ a : α, f a ⁻¹' {g a} := by
      ext; simp [funext_iff]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
α_1 : Type u_4
inst : TopologicalSpace X_1
X : Type u_5
α : Type u_6
β : Type u_7
inst_1 : Finite α
inst_2 : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
this :
  Eq.{u_5 + 1} (α := Set X) (preimage (β := (a : α) → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
    (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
⊢ IsOpen[inst_2] (preimage (β := α → β) (fun (x : X) (a : α) ↦ (f a : (a : X) → β) x) {g})
have rw : IsOpen[inst_2] (⋂ (a : α), preimage (β := β) (⇑(f a) : (a : X) → β) {g a})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), (f : (a : X) → Y) x = y
⊢ Eq (α := (g : LocallyConstant Y Z) → LocallyConstant X Z) (comap f) fun (g : LocallyConstant Y Z) ↦
    const X ((g : (a : Y) → Z) y)
have h₁ : ∀ (x : LocallyConstant Y Z) (x_1 : X),
  Eq.{u_3 + 1} (α := Z) ((comap f x : (a : X) → Z) x_1 : Z)
    (((const X ((x : (a : Y) → Z) y) : LocallyConstant X Z) : (a : X) → Z) x_1 : Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
⊢ a = b
have h₁ : ∀ (y : Y), Eq.{u_3 + 1} (α := Z) ((a : (a : Y) → Z) y : Z) ((b : (a : Y) → Z) y : Z)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
y : Y
⊢ Eq.{u_3 + 1} (α := Z) ((a : (a : Y) → Z) y : Z) ((b : (a : Y) → Z) y : Z)
have h₁ : ∀ (x : X) (hx : f.toFun x = y), Eq.{u_3 + 1} (α := Z) ((a : (a : Y) → Z) y : Z) ((b : (a : Y) → Z) y : Z)
Tactic: obtain ⟨x, hx⟩ := hfs y
-- 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
R : Type u_5
inst_1 : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst] (U.mulIndicator (⇑f : (a : X) → R) ⁻¹' s)
have rw : IsOpen[inst] ((⇑f : (a : X) → R) ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)
Tactic: rw [mulIndicator_preimage, Set.ite, Set.diff_eq]
-- 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
e : Y ≃ Z
x : LocallyConstant X Y
⊢ map.{u_1, u_3, u_2} (Y := Z) (⇑e.symm : (a : Z) → Y) (map (⇑e : (a : Y) → Z) x) = x
have 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)
Tactic: ext
-- 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
e : Y ≃ Z
x : LocallyConstant X Z
⊢ map.{u_1, u_2, u_3} (Y := Y) (⇑e : (a : Y) → Z) (map (⇑e.symm : (a : Z) → Y) x) = x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
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 := ⊥
⊢ 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 ⋯)
have this : DiscreteTopology Z
Tactic: haveI : DiscreteTopology Z := discreteTopology_bot Z
-- 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
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
⊢ 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 ⋯)
have 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 sorry) :
          Z)
        ((g : (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 (g : (a : (↑C₂ : Type u_1)) → Z) (Subtype.mk (p := fun (x : X) ↦ x ∈ C₂) i sorry)
Tactic: obtain ⟨f, hf⟩ := f
Cleared hypotheses: f, hfg