awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
⊢ ∃ y ∈ E ∩ D, y ≠ x
have this : ¬(E ∩ D).Countable
Tactic: have : ¬(E ∩ D).Countable := by
      intro h
      obtain ⟨U, hUb, xU, hU⟩ : ∃ U ∈ b, x ∈ U ∧ U ⊆ E :=
        (IsTopologicalBasis.mem_nhds_iff bbasis).mp xE
      have hU_cnt : (U ∩ C).Countable := by
        apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)
        · rintro y ⟨yU, yC⟩
          by_cases h : y ∈ V
          · exact mem_union_right _ (mem_inter h yC)
          · exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)
        exact Countable.union h Vct
      have : U ∈ v := ⟨hUb, hU_cnt⟩
      apply xD.2
      exact mem_biUnion this xU
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬(E ∩ D).Countable
⊢ ∃ y ∈ E ∩ D, y ≠ x
have refine_2 : ∀ (h : ∀ (y : α) (_ : y ∈ E ∩ D), y = x), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ C = V ∩ C ∪ D
have refine_3 : C = C ∩ V ∪ D
Tactic: rw [inter_comm, inter_union_diff]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
b : Set (Set α)
bct : b.Countable
left : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U : Set α | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
refine_3 : C = C ∩ V ∪ D
⊢ C = V ∩ C ∪ D
have refine_3₁ : C = C
Tactic: rw [inter_comm, inter_union_diff]
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
⊢ ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C
have rcases : ∀ (V D : Set α) (Vct : V.Countable) (Dperf : Perfect D) (VD : C = V ∪ D), ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C
Tactic: rcases exists_countable_union_perfect_of_isClosed hclosed with ⟨V, D, Vct, Dperf, VD⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ ∃ (D : Set α), Perfect D ∧ D.Nonempty ∧ D ⊆ C
have refine : D.Nonempty ∧ D ⊆ C
Tactic: refine ⟨D, ⟨Dperf, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty ∧ D ⊆ C
have left : D.Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
left : D.Nonempty
⊢ D.Nonempty ∧ D ⊆ C
have right : D ⊆ C
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty
have left : D ≠ ∅
Tactic: rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Topology.Perfect (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
⊢ False
have VD₁ : C = V
Tactic: rw [h, union_empty] at VD
Cleared hypotheses: VD, h
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
have left : ∀ (hunc : ¬V.Countable) (D : Set α) (Vct : V.Countable) (Dperf : Perfect D) (VD : C = V) (h : D = ∅), False
Tactic: rw [VD] at hunc
Cleared hypotheses: hunc, D, Vct, Dperf, VD, h
-- Lean 4 proof step from Mathlib.Topology.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
C : Set α
inst_1 : SecondCountableTopology α
hclosed : IsClosed[inst] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C
have right : D ⊆ V ∪ D
Tactic: rw [VD]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
have rw : ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
Tactic: rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
rw :
  ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
have rw₁ : Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 (update (β := fun (a : α) ↦ β) f x y x)) ↔
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
Tactic: rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
rw :
  ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
rw₁ :
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 (update (β := fun (a : α) ↦ β) f x y x)) ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
have rw₂ : Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y) ↔
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
Tactic: rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
have rw : ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
Tactic: { rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self] }
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
rw :
  ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
have rw₁ : Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 (update (β := fun (a : α) ↦ β) f x y x)) ↔
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
Tactic: { rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self] }
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
inst_2 : DecidableEq α
y : β
rw :
  ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) (s \ {x}) x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
rw₁ :
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 (update (β := fun (a : α) ↦ β) f x y x)) ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
⊢ ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) s x ↔
    Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
have rw₂ : Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y) ↔
  Tendsto (update (β := fun (a : α) ↦ β) f x y) (𝓝[s \ {x}] x) (𝓝 y)
Tactic: { rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self] }
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
inst_2 : DecidableEq α
y : β
⊢ ContinuousAt (update (β := fun (a : α) ↦ β) f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
have rw : ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) univ x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
Tactic: rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
inst_2 : DecidableEq α
y : β
rw : ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) univ x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
⊢ ContinuousAt (update (β := fun (a : α) ↦ β) f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
have rw₁ : Tendsto f (𝓝[univ \ {x}] x) (𝓝 y) ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
Tactic: rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
inst_2 : DecidableEq α
y : β
rw : ContinuousWithinAt (update (β := fun (a : α) ↦ β) f x y) univ x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
rw₁ : Tendsto f (𝓝[univ \ {x}] x) (𝓝 y) ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
⊢ ContinuousAt (update (β := fun (a : α) ↦ β) f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
have rw₂ : Tendsto f (𝓝[univ \ {x}] x) (𝓝 y) ↔ Tendsto f (𝓝[univ \ {x}] x) (𝓝 y)
Tactic: rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx : x ∈ s
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s x
have pos : ∀ (hx' : Membership.mem (γ := Set α) (frontier {a : α | p a}) x),
  ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s x
Tactic: by_cases hx' : x ∈ frontier { a | p a }
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx : x ∈ s
pos :
  ∀ (hx' : Membership.mem (γ := Set α) (frontier {a : α | p a}) x),
    ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s x
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s x
have neg : ∀ (hx' : x ∉ frontier {a : α | p a}),
  ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s x
Tactic: by_cases hx' : x ∈ frontier { a | p a }
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx : x ∈ s
hx' : x ∉ frontier {a : α | p a}
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s x
have neg : ∀ (hx : x ∈ s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) (hx' : x ∉ frontier {a : α | p a}),
  ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
Tactic: rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢
Cleared hypotheses: hx, hx'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx : x ∈ s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ
hx' : x ∉ frontier {a : α | p a}
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
have neg : ∀ (hx : x ∈ s ∩ {a : α | p a}),
  ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx : x ∈ s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ
hx' : x ∉ frontier {a : α | p a}
neg :
  ∀ (hx : x ∈ s ∩ {a : α | p a}),
    ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
      (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
have neg₁ : ∀ (hx : x ∈ s ∩ {a : α | p a}ᶜ),
  ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx' : x ∉ frontier {a : α | p a}
hx : x ∈ s ∩ {a : α | p a}
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
have neg : ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}) x
Tactic: apply ContinuousWithinAt.union
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx' : x ∉ frontier {a : α | p a}
hx : x ∈ s ∩ {a : α | p a}
neg : ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}) x
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
have neg₁ : ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}ᶜ) x
Tactic: apply ContinuousWithinAt.union
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx' : x ∉ frontier {a : α | p a}
hx : x ∈ s ∩ {a : α | p a}
h : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}ᶜ) x
⊢ x ∉ interior {a : α | p a}
have rwa : ∀ (h : Membership.mem (γ := Set α) (interior {a : α | p a})ᶜ x), x ∉ interior {a : α | p a}
Tactic: rwa [closure_compl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Piecewise (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx' : x ∉ frontier {a : α | p a}
hx : x ∈ s ∩ {a : α | p a}
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}ᶜ) x
have this : x ∉ closure[inst] {a : α | p a}ᶜ
Tactic: have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx' : x ∉ frontier {a : α | p a}
hx : x ∈ s ∩ {a : α | p a}ᶜ
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
have neg : ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}) x
Tactic: apply ContinuousWithinAt.union
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx' : x ∉ frontier {a : α | p a}
hx : x ∈ s ∩ {a : α | p a}ᶜ
neg : ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}) x
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a)
    (s ∩ {a : α | p a} ∪ s ∩ {a : α | p a}ᶜ) x
have neg₁ : ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}ᶜ) x
Tactic: apply ContinuousWithinAt.union
-- Lean 4 proof step from Mathlib.Topology.Piecewise (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst_2 : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a : α | p a})
hg : ContinuousOn g (s ∩ {a : α | ¬p a})
x : α
hx' : x ∉ frontier {a : α | p a}
hx : x ∈ s ∩ {a : α | p a}ᶜ
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) (s ∩ {a : α | p a}) x
have this : x ∉ closure[inst] {a : α | p a}
Tactic: have : x ∉ closure { a | p a } := fun h =>
          hx' ⟨h, fun h' : x ∈ interior { a | p a } => hx.2 (interior_subset h')⟩
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s
have hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
Tactic: apply ContinuousOn.if'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s
have hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
Tactic: apply ContinuousOn.if'