α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (fun x => h x (f x / g x)) a
show ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
case pos
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a

case neg
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
by_cases hga : g a = 0
case pos
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x => (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun x => (x, f x / g x)) a))
case pos
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
rw [ContinuousAt]
case pos
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x => (x, f x / g x)) (𝓝 a) (𝓝 ((↿h) (a, 0)))
case pos
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x => (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun x => (x, f x / g x)) a))
simp_rw [comp_apply, hga, div_zero]
no goals
case pos
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x => (x, f x / g x)) (𝓝 a) (𝓝 ((↿h) (a, 0)))
exact (h2h hga).comp (continuousAt_id.prod_mk tendsto_top)
no goals
case neg
α : Type u_1
β : Type u_3
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
exact ContinuousAt.comp (hh hga) (continuousAt_id.prod (hf.div hg hga))