-- Mathlib/Topology/LocallyFinite.lean
theorem continuousOn_iUnion' {g : X → Y} (hf : LocallyFinite f)
    (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) :
    ContinuousOn g (⋃ i, f i)

Proof state:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
intro i

Result:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Proof state:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx

Result:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Proof state:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
by_cases hx : x ∈ closure (f i)

Result:
case pos
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Proof state:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))

Tactic:
exact tendsto_bot

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
⊢ ContinuousOn g (⋃ i, f i)

Tactic:
rintro x -

Result:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ i, f i) x

Proof state:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ i, f i) x

Tactic:
rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]

Result:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))

Proof state:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
rw [hx]

Result:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))

Proof state:
case pos
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
exact hc i _ hx

Result:
no goals