awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : Zero G₀
inst_1 : Inv G₀
inst_2 : TopologicalSpace G₀
inst_3 : ContinuousInv₀ G₀
f : α → G₀
s : Set α
a : α
inst_4 : TopologicalSpace α
hf : ContinuousWithinAt f s a
ha : f a ≠ 0
⊢ ContinuousWithinAt.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ (f x)⁻¹) s a

Tactic:
hf.inv₀ ha

Premises used: ContinuousWithinAt, Filter.Tendsto.inv₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : Zero G₀
inst_1 : Inv G₀
inst_2 : TopologicalSpace G₀
inst_3 : ContinuousInv₀ G₀
f : α → G₀
a : α
inst_4 : TopologicalSpace α
hf : ContinuousAt f a
ha : f a ≠ 0
⊢ ContinuousAt.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ (f x)⁻¹) a

Tactic:
hf.inv₀ ha

Premises used: ContinuousAt, Filter.Tendsto.inv₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : Zero G₀
inst_1 : Inv G₀
inst_2 : TopologicalSpace G₀
inst_3 : ContinuousInv₀ G₀
f : α → G₀
inst_4 : TopologicalSpace α
hf : Continuous[inst_4, inst_2] f
h0 : ∀ (x : α), f x ≠ 0
⊢ Continuous[inst_4, inst_2] fun (x : α) ↦ (f x)⁻¹

Tactic:
continuous_iff_continuousAt.2 fun x => (hf.tendsto x).inv₀ (h0 x)

Premises used: Iff.mpr, Continuous.tendsto, Filter.Tendsto.inv₀, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : Zero G₀
inst_1 : Inv G₀
inst_2 : TopologicalSpace G₀
inst_3 : ContinuousInv₀ G₀
f : α → G₀
s : Set α
inst_4 : TopologicalSpace α
hf : ContinuousOn f s
h0 : ∀ x ∈ s, f x ≠ 0
⊢ ContinuousOn.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ (f x)⁻¹) s

Tactic:
fun x hx => (hf x hx).inv₀ (h0 x hx)

Premises used: ContinuousWithinAt.inv₀, ContinuousOn
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
⊢ IsEmbedding.{u_3, u_3} (X := G₀ˣ) val

Tactic:
embedding_val_mk <| (continuousOn_inv₀ (G₀ := G₀)).mono fun _ ↦ IsUnit.ne_zero

Premises used: continuousOn_inv₀, Units.embedding_val_mk, ContinuousOn.mono, IsUnit.ne_zero
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
x : G₀
⊢ (∃ (x_1 : G₀), x_1 ≠ 0 ∧ x_1 = x) ↔ Membership.mem (γ := Set G₀) {g : G₀ | g = 0 → False} x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
x : { g : G₀ // g ≠ 0 }
⊢ (fun (g : { g : G₀ // g ≠ 0 }) ↦ (Subtype.mk (p := fun (g : G₀) ↦ g ≠ 0) (↑g : G₀)⁻¹ ⋯ : { g : G₀ // g ≠ 0 }))
      ((fun (g : { g : G₀ // g ≠ 0 }) ↦ (Subtype.mk (p := fun (g : G₀) ↦ g ≠ 0) (↑g : G₀)⁻¹ ⋯ : { g : G₀ // g ≠ 0 }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ 𝓝 x⁻¹ = (𝓝 x)⁻¹

Tactic:
le_antisymm (inv_le_iff_le_inv.1 ?_) (tendsto_inv₀ hx)

Premises used: le_antisymm, Iff.mp, tendsto_inv₀, Filter.inv_le_iff_le_inv
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
refine : (𝓝 x⁻¹)⁻¹ ≤ 𝓝 x
⊢ 𝓝 x⁻¹ = (𝓝 x)⁻¹

Tactic:
refine le_antisymm (inv_le_iff_le_inv.1 ?_) (tendsto_inv₀ hx)

Premises used: le_antisymm, Iff.mp, tendsto_inv₀, Filter.inv_le_iff_le_inv
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ (𝓝 x⁻¹)⁻¹ ≤ 𝓝 x

Tactic:
simpa only [inv_inv] using tendsto_inv₀ (inv_ne_zero hx)

Premises used: inv_inv, inv_ne_zero, tendsto_inv₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
x : G₀
l : Filter α
f : α → G₀
hx : x ≠ 0
⊢ Tendsto (fun (x : α) ↦ (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x)

Tactic:
simp only [nhds_inv₀ hx, ← Filter.comap_inv, tendsto_comap_iff, Function.comp_def, inv_inv]

Premises used: Filter.tendsto_comap_iff, nhds_inv₀, Function.comp_def, Filter.comap_inv, inv_inv
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : 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))

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ hy)

Premises used: div_eq_mul_inv, Filter.Tendsto.mul, Filter.Tendsto.inv₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : 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)

Tactic:
⟨fun hfg => ?_, fun hf => hf.mul hg⟩

Premises used: Filter.Tendsto.mul, Iff.intro
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
refine : ∀ (hfg : Tendsto (fun (n : α) ↦ f n * g n) l (𝓝 (x * y))), Tendsto f l (𝓝 x)
⊢ Tendsto (fun (n : α) ↦ f n * g n) l (𝓝 (x * y)) ↔ Tendsto f l (𝓝 x)

Tactic:
refine ⟨fun hfg => ?_, fun hf => hf.mul hg⟩
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : 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))
rw : Tendsto f l (𝓝 (x * y / y))
⊢ Tendsto f l (𝓝 x)

Tactic:
rw [← mul_div_cancel_right₀ x hy]

Premises used: mul_div_cancel_right₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : 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))

Tactic:
Tendsto.congr' ?_ (hfg.div hg hy)

Premises used: Filter.Tendsto.div, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : 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))
refine : (fun (n : α) ↦ f n * g n) / g =ᶠ[l] f
⊢ Tendsto f l (𝓝 (x * y / y))

Tactic:
refine Tendsto.congr' ?_ (hfg.div hg hy)

Premises used: Filter.Tendsto.div, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : 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

Tactic:
(hg.eventually_ne hy).mono fun n hn => mul_div_cancel_right₀ _ hn

Premises used: Filter.Tendsto.eventually_ne, Filter.EventuallyEq, Filter.Eventually.mono, mul_div_cancel_right₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : 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

Tactic:
exact (hg.eventually_ne hy).mono fun n hn => mul_div_cancel_right₀ _ hn

Premises used: Filter.Tendsto.eventually_ne, Filter.Eventually.mono, mul_div_cancel_right₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f g : α → G₀
inst_4 : TopologicalSpace α
s : Set α
a : α
hf : ContinuousWithinAt f s a
hg : ContinuousWithinAt g s a
h₀ : g a ≠ 0
⊢ ContinuousWithinAt (f / g) s a

Tactic:
hf.div hg h₀

Premises used: ContinuousWithinAt, Filter.Tendsto.div
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f g : α → G₀
inst_4 : TopologicalSpace α
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
h₀ : ∀ x ∈ s, g x ≠ 0
⊢ ContinuousOn (f / g) s

Tactic:
fun x hx => (hf x hx).div (hg x hx) (h₀ x hx)

Premises used: ContinuousOn, ContinuousWithinAt.div
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f g : α → G₀
inst_4 : TopologicalSpace α
a : α
hf : ContinuousAt f a
hg : ContinuousAt g a
h₀ : g a ≠ 0
⊢ ContinuousAt (f / g) a

Tactic:
hf.div hg h₀

Premises used: ContinuousAt, Filter.Tendsto.div
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f g : α → G₀
inst_4 : TopologicalSpace α
hf : Continuous[inst_4, inst_1] f
hg : Continuous[inst_4, inst_1] g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous[inst_4, inst_1] (f / g)

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Premises used: div_eq_mul_inv, Continuous.mul, Continuous.inv₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
⊢ ContinuousOn (Y := G₀) (fun (p : G₀ × G₀) ↦ p.1 / p.2) {p : G₀ × G₀ | p.2 ≠ 0}

Tactic:
continuousOn_fst.div continuousOn_snd fun _ => id

Premises used: id, ContinuousOn.div, continuousOn_snd, continuousOn_fst
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f g : α → G₀
inst_4 : TopologicalSpace α
hf : Continuous[inst_4, inst_1] f
hg : Continuous[inst_4, inst_1] g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous[inst_4, inst_1] fun (x : α) ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Premises used: div_eq_mul_inv, Continuous.mul, Continuous.inv₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f g : α → G₀
inst_4 : TopologicalSpace α
a : α
hf : ContinuousAt f a
hg : ContinuousAt g a
h₀ : g a ≠ 0
⊢ ContinuousAt.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ f x / g x) a

Tactic:
ContinuousAt.div hf hg h₀

Premises used: ContinuousAt.div
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f g : α → G₀
inst_4 : TopologicalSpace α
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
h₀ : ∀ x ∈ s, g x ≠ 0
⊢ ContinuousOn.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ f x / g x) s

Tactic:
ContinuousOn.div hf hg h₀

Premises used: ContinuousOn.div
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
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) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
change : ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
⊢ ContinuousAt.{u_1, u_2} (Y := β) (fun (x : α) ↦ h x (f x / g x)) a

Tactic:
change ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a

Premises used: ContinuousAt, Function.comp, HDiv.hDiv, Prod.mk, Function.HasUncurry.uncurry
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
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) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
pos : ∀ (hga : g a = 0), ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
neg : ∀ (hga : ¬g a = 0), ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
⊢ ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a

Tactic:
by_cases hga : g a = 0
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
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) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
hga : g a = 0
pos : Tendsto (↿h ∘ fun (x : α) ↦ (x, f x / g x)) (𝓝 a) (𝓝 (↿h (a, 0)))
⊢ Tendsto (↿h ∘ fun (x : α) ↦ (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun (x : α) ↦ (x, f x / g x)) a))

Tactic:
simp_rw [comp_apply, hga, div_zero]

Premises used: Function.comp_apply, div_zero
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
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) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun (x : α) ↦ (x, f x / g x)) (𝓝 a) (𝓝 (↿h (a, 0)))

Tactic:
(h2h hga).comp (continuousAt_id.tendsto.prodMk tendsto_top)

Premises used: ContinuousAt.tendsto, Filter.tendsto_top, Filter.Tendsto.prodMk, Filter.Tendsto.comp, continuousAt_id
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
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) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun (x : α) ↦ (x, f x / g x)) (𝓝 a) (𝓝 (↿h (a, 0)))

Tactic:
exact (h2h hga).comp (continuousAt_id.tendsto.prodMk tendsto_top)

Premises used: ContinuousAt.tendsto, Filter.tendsto_top, Filter.Tendsto.prodMk, Filter.Tendsto.comp, continuousAt_id
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
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) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
hga : ¬g a = 0
funProp funProp₁ : g a ≠ 0
⊢ ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
f g : α → G₀
h : α → G₀ → β
hf : Continuous[inst_4, inst_1] f
hg : Continuous[inst_4, inst_1] g
hh : ∀ (a : α), g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : ∀ (a : α), g a = 0 → Tendsto (↿h) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
⊢ Continuous[inst_4, inst_5] fun (x : α) ↦ h x (f x / g x)

Tactic:
continuous_iff_continuousAt.mpr fun a =>
    hf.continuousAt.comp_div_cases _ hg.continuousAt (hh a) (h2h a)

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.comp_div_cases, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : GroupWithZero α
inst_2 : SeparatelyContinuousMul α
c : α
hc : c ≠ 0
⊢ Eq (α := (a : α) → α) (⇑(Homeomorph.mulLeft₀ c hc) : (a : α) → α) fun (x : α) ↦ c * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : GroupWithZero α
inst_2 : SeparatelyContinuousMul α
c : α
hc : c ≠ 0
⊢ Eq (α := (a : α) → α) (⇑(Homeomorph.symm (Homeomorph.mulLeft₀ c hc)) : (a : α) → α) fun (x : α) ↦ c⁻¹ * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : GroupWithZero α
inst_2 : SeparatelyContinuousMul α
c : α
hc : c ≠ 0
⊢ Eq (α := (a : α) → α) (⇑(Homeomorph.mulRight₀ c hc) : (a : α) → α) fun (x : α) ↦ x * c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : GroupWithZero α
inst_2 : SeparatelyContinuousMul α
c : α
hc : c ≠ 0
⊢ Eq (α := (a : α) → α) (⇑(Homeomorph.symm (Homeomorph.mulRight₀ c hc)) : (a : α) → α) fun (x : α) ↦ x * c⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
b : G₀
⊢ map (fun (x : G₀) ↦ a * x) (𝓝 b) = 𝓝 (a * b)

Tactic:
(Homeomorph.mulLeft₀ a ha).map_nhds_eq b

Premises used: Homeomorph.mulLeft₀, Homeomorph.map_nhds_eq
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
rw : 𝓝 (a * 1) = 𝓝 a
rw₁ rw₂ : 𝓝 a = 𝓝 a
⊢ map (fun (x : G₀) ↦ a * x) (𝓝 1) = 𝓝 a

Tactic:
rw [map_mul_left_nhds₀ ha, mul_one]

Premises used: mul_one, map_mul_left_nhds₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
b : G₀
⊢ map (fun (x : G₀) ↦ x * a) (𝓝 b) = 𝓝 (b * a)

Tactic:
(Homeomorph.mulRight₀ a ha).map_nhds_eq b

Premises used: Homeomorph.map_nhds_eq, Homeomorph.mulRight₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
rw : 𝓝 (1 * a) = 𝓝 a
rw₁ rw₂ : 𝓝 a = 𝓝 a
⊢ map (fun (x : G₀) ↦ x * a) (𝓝 1) = 𝓝 a

Tactic:
rw [map_mul_right_nhds₀ ha, one_mul]

Premises used: map_mul_right_nhds₀, one_mul
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 ((Homeomorph.symm (Homeomorph.symm (Homeomorph.mulRight₀ a ha)) : (a : G₀) → G₀) 1) = 𝓝 a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
h : Tendsto.{u_3, u_3} (α := G₀) Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
⊢ x⁻¹ ≠ 0

Tactic:
have hx' := inv_ne_zero hx
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
h : Tendsto.{u_3, u_3} (α := G₀) Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
rw :
  Tendsto.{u_3, u_3} (α := G₀) (β := G₀) ((fun (x_1 : G₀) ↦ x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun (x_1 : G₀) ↦ x * x_1) (𝓝 1)
    (𝓝 1)
⊢ ContinuousAt Inv.inv x

Tactic:
rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx',
      tendsto_map'_iff, tendsto_comap_iff]

Premises used: map_mul_left_nhds_one₀, ContinuousAt, Filter.tendsto_map'_iff, nhds_translation_mul_inv₀, Filter.tendsto_comap_iff
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
h : Tendsto.{u_3, u_3} (α := G₀) Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto.{u_3, u_3} (α := G₀) (β := G₀) ((fun (x_1 : G₀) ↦ x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun (x_1 : G₀) ↦ x * x_1) (𝓝 1)
    (𝓝 1)

Tactic:
simpa only [Function.comp_def, mul_inv_rev, mul_inv_cancel_right₀ hx']

Premises used: mul_inv_cancel_right₀, Function.comp_def, mul_inv_rev
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℤ
h : x ≠ 0 ∨ 0 ≤ m
ofNat : ∀ (m : ℕ) (h : x ≠ 0 ∨ 0 ≤ Int.ofNat m), ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.ofNat m) x
negSucc : ∀ (m : ℕ) (h : x ≠ 0 ∨ 0 ≤ Int.negSucc m), ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.negSucc m) x
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ m) x

Tactic:
rcases m with m | m
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.ofNat m) x

Tactic:
simpa only [Int.ofNat_eq_natCast, zpow_natCast] using continuousAt_pow x m

Premises used: zpow_natCast, Int.ofNat_eq_natCast, continuousAt_pow
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
negSucc : ContinuousAt (Y := G₀) (fun (x : G₀) ↦ (x ^ (m + 1))⁻¹) x
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.negSucc m) x

Tactic:
simp only [zpow_negSucc]

Premises used: zpow_negSucc
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_ge
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ (x ^ (m + 1))⁻¹) x

Tactic:
(continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)

Premises used: pow_ne_zero, HAdd.hAdd, ContinuousAt.inv₀, OfNat.ofNat, continuousAt_pow
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ (x ^ (m + 1))⁻¹) x

Tactic:
exact (continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)

Premises used: pow_ne_zero, HAdd.hAdd, ContinuousAt.inv₀, OfNat.ofNat, continuousAt_pow
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
m : ℤ
⊢ ContinuousOn (Y := G₀) (fun (x : G₀) ↦ x ^ m) {0}ᶜ

Tactic:
fun _x hx =>
  (continuousAt_zpow₀ _ _ (Or.inl hx)).continuousWithinAt

Premises used: continuousAt_zpow₀, ContinuousAt.continuousWithinAt, ContinuousOn, Or.inl
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
f : α → G₀
l : Filter α
a : G₀
hf : Tendsto f l (𝓝 a)
m : ℤ
h : a ≠ 0 ∨ 0 ≤ m
⊢ Tendsto (fun (x : α) ↦ f x ^ m) l (𝓝 (a ^ m))

Tactic:
(continuousAt_zpow₀ _ m h).tendsto.comp hf

Premises used: continuousAt_zpow₀, ContinuousAt.tendsto, Filter.Tendsto.comp