awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Piecewise
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)
rw₂ rw₃ : Tendsto f (𝓝[univ \ {x}] x) (𝓝 y) ↔ Tendsto f (𝓝[univ \ {x}] x) (𝓝 y)
⊢ ContinuousAt (update (β := fun (a : α) ↦ β) f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)

Tactic:
rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]

Premises used: continuousWithinAt_univ, Set.compl_eq_univ_diff, continuousWithinAt_update_same
-- Module: Mathlib.Topology.Piecewise
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
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
⊢ 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 }

Premises used: frontier, setOf
-- Module: Mathlib.Topology.Piecewise
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' : 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:
(hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)

Premises used: ContinuousWithinAt, Set.Mem, setOf, And.intro, Filter.Tendsto.piecewise_nhdsWithin, Set.piecewise
-- Module: Mathlib.Topology.Piecewise
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' : 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:
exact (hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)

Premises used: And.intro, Filter.Tendsto.piecewise_nhdsWithin
-- Module: Mathlib.Topology.Piecewise
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}
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
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s x

Tactic:
rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢

Premises used: Set.inter_univ, setOf, Set.union_compl_self, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Piecewise
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
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

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.Topology.Piecewise
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
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

Tactic:
apply ContinuousWithinAt.union

Premises used: ContinuousWithinAt.union
-- Module: Mathlib.Topology.Piecewise
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

Tactic:
(hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)

Premises used: if_pos, And.right, ContinuousWithinAt.congr
-- Module: Mathlib.Topology.Piecewise
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

Tactic:
exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)

Premises used: if_pos, And.right, ContinuousWithinAt.congr
-- Module: Mathlib.Topology.Piecewise
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : Membership.mem (γ := Set α) (interior {a : α | p a})ᶜ x), x ∉ interior {a : α | p a}
⊢ x ∉ interior {a : α | p a}

Tactic:
rwa [closure_compl] at h

Premises used: closure_compl
-- Module: Mathlib.Topology.Piecewise
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}
⊢ 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⟩
-- Module: Mathlib.Topology.Piecewise
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}
this : x ∉ closure[inst] {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

Tactic:
continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Premises used: Compl.compl, setOf, continuousWithinAt_of_notMem_closure, closure_inter_subset_inter_closure, And.right
-- Module: Mathlib.Topology.Piecewise
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}
this : x ∉ closure[inst] {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

Tactic:
exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Premises used: Compl.compl, setOf, continuousWithinAt_of_notMem_closure, closure_inter_subset_inter_closure, And.right
-- Module: Mathlib.Topology.Piecewise
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
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

Tactic:
apply ContinuousWithinAt.union

Premises used: ContinuousWithinAt.union
-- Module: Mathlib.Topology.Piecewise
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}ᶜ
⊢ 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')⟩
-- Module: Mathlib.Topology.Piecewise
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}ᶜ
this : x ∉ closure[inst] {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

Tactic:
continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Premises used: setOf, continuousWithinAt_of_notMem_closure, closure_inter_subset_inter_closure, And.right
-- Module: Mathlib.Topology.Piecewise
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}ᶜ
this : x ∉ closure[inst] {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

Tactic:
exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Premises used: setOf, continuousWithinAt_of_notMem_closure, closure_inter_subset_inter_closure, And.right
-- Module: Mathlib.Topology.Piecewise
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

Tactic:
(hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Premises used: Set.Mem, setOf, And.right, if_neg, ContinuousWithinAt.congr
-- Module: Mathlib.Topology.Piecewise
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

Tactic:
exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Premises used: And.right, if_neg, ContinuousWithinAt.congr
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s t : Set α
inst_2 : (a : α) → Decidable (a ∈ t)
hpf : ∀ a ∈ s ∩ frontier t, Tendsto f (𝓝[s ∩ t] a) (𝓝 (t.piecewise (β := fun (i : α) ↦ β) f g a))
hpg : ∀ a ∈ s ∩ frontier t, Tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (t.piecewise (β := fun (i : α) ↦ β) f g a))
hf : ContinuousOn f (s ∩ t)
hg : ContinuousOn g (s ∩ tᶜ)
⊢ ContinuousOn (t.piecewise (β := fun (a : α) ↦ β) f g) s

Tactic:
hf.if' hpf hpg hg

Premises used: ContinuousOn.if', Set.piecewise
-- Module: Mathlib.Topology.Piecewise
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))
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})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s

Tactic:
apply ContinuousOn.if'

Premises used: ContinuousOn.if'
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
hpf : Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (f a))
⊢ Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))

Tactic:
simp only [← hp a ha, ite_self]

Premises used: ite_self
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
hpf : Tendsto f (𝓝[s ∩ closure[inst] {a : α | p a}] a) (𝓝 (f a))
⊢ Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (f a))

Tactic:
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)

Premises used: Set.inter_subset_inter_right, tendsto_nhdsWithin_mono_left, subset_closure
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ Tendsto f (𝓝[s ∩ closure[inst] {a : α | p a}] a) (𝓝 (f a))

Tactic:
hf a ⟨ha.1, ha.2.1⟩

Premises used: ContinuousWithinAt, And.right, And.left, And.intro
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ Tendsto f (𝓝[s ∩ closure[inst] {a : α | p a}] a) (𝓝 (f a))

Tactic:
exact hf a ⟨ha.1, ha.2.1⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
hpg : Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (g a))
⊢ Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))

Tactic:
simp only [hp a ha, ite_self]

Premises used: ite_self
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
hpg : Tendsto g (𝓝[s ∩ closure[inst] {a : α | ¬p a}] a) (𝓝 (g a))
⊢ Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (g a))

Tactic:
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)

Premises used: Set.inter_subset_inter_right, tendsto_nhdsWithin_mono_left, subset_closure
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ a ∈ s

Tactic:
rcases ha with ⟨has, ⟨_, ha⟩⟩
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
has : a ∈ s
⊢ Membership.mem (γ := Set α) (closure[inst] {a : α | p a}) a

Tactic:
rcases ha with ⟨has, ⟨_, ha⟩⟩
-- Module: Mathlib.Topology.Piecewise
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})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
has : a ∈ s
left : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}) a
⊢ a ∉ interior {a : α | p a}

Tactic:
rcases ha with ⟨has, ⟨_, ha⟩⟩
-- Module: Mathlib.Topology.Piecewise
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})
a : α
has : a ∈ s
left : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}) a
ha : a ∉ interior {a : α | p a}
⊢ Membership.mem (γ := Set α) (closure[inst] {a : α | p a}ᶜ) a

Tactic:
rw [← mem_compl_iff, ← closure_compl] at ha

Premises used: closure_compl, Set.mem_compl_iff
-- Module: Mathlib.Topology.Piecewise
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})
a : α
has : a ∈ s
left : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}) a
ha : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}ᶜ) a
⊢ Tendsto g (𝓝[s ∩ closure[inst] {a : α | ¬p a}] a) (𝓝 (g a))

Tactic:
apply hg a ⟨has, ha⟩

Premises used: And.intro