[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : DivInvMonoid G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousMul G₀
f : α → G₀
s : Set α
l : Filter α
x : G₀
hf : Tendsto f l (𝓝 x)
y : G₀
⊢ Tendsto (fun a => f a / y) l (𝓝 (x / y))
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul tendsto_const_nhds
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : DivInvMonoid G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousMul G₀
f : α → G₀
s : Set α
l : Filter α
inst✝ : TopologicalSpace α
hf : ContinuousOn f s
y : G₀
⊢ ContinuousOn (fun x => f x / y) s
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul continuousOn_const
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : DivInvMonoid G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousMul G₀
f : α → G₀
s : Set α
l : Filter α
inst✝ : TopologicalSpace α
hf : Continuous f
y : G₀
⊢ Continuous fun x => f x / y
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul continuous_const
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
f g : α → G₀
l : Filter α
a b : G₀
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
hy : b ≠ 0
⊢ Tendsto (f / g) l (𝓝 (a / b))
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ hy)
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
⊢ Tendsto (fun n => f n * g n) l (𝓝 (x * y)) ↔ Tendsto f l (𝓝 x)
[PROOFSTEP]
refine' ⟨fun hfg => _, fun hf => hf.mul hg⟩
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 x)
[PROOFSTEP]
rw [← mul_div_cancel x hy]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))
[PROOFSTEP]
refine' Tendsto.congr' _ (hfg.div hg hy)
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ (fun n => f n * g n) / g =ᶠ[l] f
[PROOFSTEP]
refine' (hg.eventually_ne hy).mono fun n hn => mul_div_cancel _ hn
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f g : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
hf : Continuous f
hg : Continuous g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous (f / g)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
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
[PROOFSTEP]
show ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
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
[PROOFSTEP]
by_cases hga : g a = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
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
[PROOFSTEP]
rw [ContinuousAt]
[GOAL]
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
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))
[PROOFSTEP]
simp_rw [comp_apply, hga, div_zero]
[GOAL]
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
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)))
[PROOFSTEP]
exact (h2h hga).comp (continuousAt_id.prod_mk tendsto_top)
[GOAL]
case neg
α : Type u_1
β : Type u_2
G₀ : Type u_3
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
[PROOFSTEP]
exact ContinuousAt.comp (hh hga) (continuousAt_id.prod (hf.div hg hga))
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x => a * x) (𝓝 1) = 𝓝 a
[PROOFSTEP]
rw [map_mul_left_nhds₀ ha, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x => x * a) (𝓝 1) = 𝓝 a
[PROOFSTEP]
rw [map_mul_right_nhds₀ ha, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 (↑(Homeomorph.symm (Homeomorph.symm (Homeomorph.mulRight₀ a ha))) 1) = 𝓝 a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
have hx' := inv_ne_zero hx
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx', tendsto_map'_iff, tendsto_comap_iff]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto ((fun x_1 => x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun x_1 => x * x_1) (𝓝 1) (𝓝 1)
[PROOFSTEP]
simpa only [(· ∘ ·), mul_inv_rev, mul_inv_cancel_right₀ hx']
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℤ
h : x ≠ 0 ∨ 0 ≤ m
⊢ ContinuousAt (fun x => x ^ m) x
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x => x ^ Int.ofNat m) x
[PROOFSTEP]
simpa only [Int.ofNat_eq_coe, zpow_coe_nat] using continuousAt_pow x m
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => x ^ Int.negSucc m) x
[PROOFSTEP]
simp only [zpow_negSucc]
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
[PROOFSTEP]
have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_le
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
[PROOFSTEP]
exact (continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)
