-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.if {p : α → Prop} [∀ a, Decidable (p a)]
    (hp : ∀ a ∈ s ∩ frontier { a | p a }, f a = g a)
    (hf : ContinuousOn f <| s ∩ closure { a | p a })
    (hg : ContinuousOn g <| s ∩ closure { a | ¬p a }) :
    ContinuousOn (fun a => if p a then f a else g a) s

Proof state:
case hpf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (f a))

Tactic:
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)

Result:
case hpf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto f (𝓝[s ∩ closure {a | p a}] a) (𝓝 (f a))

Proof state:
case hpg.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : a ∈ closure {a | p a}ᶜ
⊢ Tendsto g (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))

Tactic:
apply hg a ⟨has, ha⟩

Result:
no goals

Proof state:
case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto g (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))

Tactic:
rcases ha with ⟨has, ⟨_, ha⟩⟩

Result:
case hpg.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : a ∉ interior {a | p a}
⊢ Tendsto g (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))

Proof state:
case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))

Tactic:
rintro a ha

Result:
case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))