awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
x : α
⊢ ContinuousAt f⁻¹ x ↔ ContinuousAt f x

Tactic:
(Homeomorph.inv G).comp_continuousAt_iff _ _

Premises used: Homeomorph.inv, Homeomorph.comp_continuousAt_iff
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
⊢ ContinuousOn f⁻¹ s ↔ ContinuousOn f s

Tactic:
(Homeomorph.inv G).comp_continuousOn_iff _ _

Premises used: Homeomorph.comp_continuousOn_iff, Homeomorph.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
a : G
⊢ Eq (α := Filter G) (map (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝[≠] a) : Filter G)
    (𝓝[image (α := G) (⇑(Homeomorph.inv G) : (a : G) → G) {a}ᶜ] (Homeomorph.inv G : (a : G) → G) a : Filter G)

Tactic:
(Homeomorph.inv G).isEmbedding.map_nhdsWithin_eq ..

Premises used: Homeomorph.isEmbedding, Homeomorph.inv, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
a : G
h : Eq (α := Set G) {a⁻¹}ᶜ (image (α := G) (⇑(Homeomorph.inv G) : (a : G) → G) {a}ᶜ)
⊢ (𝓝[≠] a)⁻¹ = 𝓝[≠] a⁻¹

Tactic:
convert! (Homeomorph.inv G).isEmbedding.map_nhdsWithin_eq .. using 2

Premises used: Homeomorph.isEmbedding, Homeomorph.inv, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
a : G
⊢ Eq (α := Set G) {a⁻¹}ᶜ (image (α := G) (⇑(Homeomorph.inv G) : (a : G) → G) {a}ᶜ)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Inv G
ts : Set (TopologicalSpace G)
h : ∀ t ∈ ts, ContinuousInv G
⊢ ContinuousInv G

Tactic:
letI := sInf ts
  { continuous_inv :=
      continuous_sInf_rng.2 fun t ht =>
        continuous_sInf_dom ht (@ContinuousInv.continuous_inv G t _ (h t ht)) }

Premises used: Iff.mpr, ContinuousInv.mk, continuous_sInf_dom, ContinuousInv.continuous_inv, continuous_sInf_rng
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
ι' : Sort u_1
inst : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G

Tactic:
continuousInv_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, Set.forall_mem_range, continuousInv_sInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
ι' : Sort u_1
inst : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G

Tactic:
exact continuousInv_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, Set.forall_mem_range, continuousInv_sInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
rw : ContinuousInv G
⊢ ContinuousInv G

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

Tactic:
continuousInv_iInf fun b => ?_

Premises used: continuousInv_iInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
refine : ∀ (b : Bool), ContinuousInv G
⊢ ContinuousInv G

Tactic:
refine continuousInv_iInf fun b => ?_

Premises used: continuousInv_iInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
b : Bool
false : ContinuousInv G
true : ContinuousInv G
⊢ ContinuousInv G

Tactic:
cases b
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Inv G
inst_1 : Inv H
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace H
inst_4 : ContinuousInv H
f : G → H
hf : IsInducing f
hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹
⊢ Continuous[inst_2, inst_3] (f ∘ fun (a : G) ↦ a⁻¹)

Tactic:
simpa only [Function.comp_def, hf_inv] using hf.continuous.inv

Premises used: Function.comp_def, Continuous.inv, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
M : Type u_1
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
⊢ ContinuousConstSMul (ConjAct Mˣ) M

Tactic:
⟨fun _ => (continuous_const.mul continuous_id).mul continuous_const⟩

Premises used: continuous_const, ContinuousConstSMul.mk, Continuous.mul, continuous_id
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : Mul G
inst_3 : ContinuousMul G
inst_4 : ContinuousInv G
⊢ Continuous[instTopologicalSpaceProd, inst] fun (g : G × G) ↦ g.1 * g.2 * g.1⁻¹

Tactic:
continuous_mul.mul (continuous_inv.comp continuous_fst)

Premises used: continuous_mul, Continuous.comp, continuous_fst, Continuous.mul, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : Mul G
inst_3 : SeparatelyContinuousMul G
g : G
⊢ Continuous[inst, inst] fun (h : G) ↦ g * h * g⁻¹

Tactic:
(continuous_mul_const g⁻¹).comp (continuous_const_mul g)

Premises used: Continuous.comp, continuous_const_mul, Inv.inv, continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : Mul G
inst_3 : ContinuousMul G
inst_4 : ContinuousInv G
h : G
⊢ Continuous[inst, inst] fun (g : G) ↦ g * h * g⁻¹

Tactic:
(continuous_mul_const h).mul continuous_inv

Premises used: Continuous.mul, ContinuousInv.continuous_inv, continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
n : ℕ
⊢ Continuous[inst, inst] fun (a : G) ↦ a ^ Int.ofNat n

Tactic:
simpa using continuous_pow n

Premises used: continuous_pow
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
n : ℕ
⊢ Continuous[inst, inst] fun (a : G) ↦ a ^ Int.negSucc n

Tactic:
simpa using (continuous_pow (n + 1)).inv

Premises used: HAdd.hAdd, Continuous.inv, OfNat.ofNat, continuous_pow
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
A : Type u_1
inst_4 : AddGroup A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalAddGroup A
⊢ ContinuousConstSMul ℤ A

Tactic:
⟨continuous_zsmul⟩

Premises used: continuous_zsmul, ContinuousConstSMul.mk
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
A : Type u_1
inst_4 : AddGroup A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalAddGroup A
⊢ ContinuousSMul ℤ A

Tactic:
⟨continuous_prod_of_discrete_left.mpr continuous_zsmul⟩

Premises used: Iff.mpr, continuous_zsmul, continuous_prod_of_discrete_left, ContinuousSMul.mk
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
h : Continuous[inst_3, inst] f
z : ℤ
⊢ Continuous[inst_3, inst] fun (b : α) ↦ f b ^ z

Tactic:
(continuous_zpow z).comp h

Premises used: continuous_zpow, Continuous.comp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
z : ℤ
⊢ ContinuousOn (Y := G) (fun (x : G) ↦ x ^ z) s

Tactic:
(continuous_zpow z).continuousOn

Premises used: continuous_zpow, Continuous.continuousOn
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
z : ℤ
⊢ ContinuousAt (Y := G) (fun (x : G) ↦ x ^ z) x

Tactic:
(continuous_zpow z).continuousAt

Premises used: continuous_zpow, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
α : Type u_1
l : Filter α
f : α → G
x : G
hf : Tendsto f l (𝓝 x)
z : ℤ
⊢ Tendsto (fun (x : α) ↦ f x ^ z) l (𝓝 (x ^ z))

Tactic:
(continuousAt_zpow _ _).tendsto.comp hf

Premises used: continuousAt_zpow, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
x : α
s : Set α
hf : ContinuousWithinAt f s x
z : ℤ
⊢ ContinuousWithinAt.{u, w} (Y := G) (fun (x : α) ↦ f x ^ z) s x

Tactic:
Filter.Tendsto.zpow hf z

Premises used: ContinuousWithinAt, Filter.Tendsto.zpow
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
x : α
hf : ContinuousAt f x
z : ℤ
⊢ ContinuousAt.{u, w} (Y := G) (fun (x : α) ↦ f x ^ z) x

Tactic:
Filter.Tendsto.zpow hf z

Premises used: ContinuousAt, Filter.Tendsto.zpow
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
hf : ContinuousOn f s
z : ℤ
⊢ ContinuousOn.{u, w} (Y := G) (fun (x : α) ↦ f x ^ z) s

Tactic:
fun x hx => (hf x hx).zpow z

Premises used: ContinuousWithinAt.zpow, ContinuousOn
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Eq (α := Filter H) (map (⇑(Homeomorph.mulLeft c) : (a : H) → H) (𝓝[>] a) : Filter H)
    (𝓝[(⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Ioi a] (Homeomorph.mulLeft c : (a : H) → H) a : Filter H)

Tactic:
(Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq ..

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.map_nhdsWithin_eq, Homeomorph.mulLeft
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
h : Ioi (c * a) = (⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Ioi a
⊢ map (fun (x : H) ↦ c * x) (𝓝[>] a) = 𝓝[>] (c * a)

Tactic:
convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.map_nhdsWithin_eq, Homeomorph.mulLeft
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Ioi (c * a) = (⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Ioi a

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Eq (α := Filter H) (map (⇑(Homeomorph.mulLeft c) : (a : H) → H) (𝓝[<] a) : Filter H)
    (𝓝[(⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Iio a] (Homeomorph.mulLeft c : (a : H) → H) a : Filter H)

Tactic:
(Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq ..

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.map_nhdsWithin_eq, Homeomorph.mulLeft
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
h : Iio (c * a) = (⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Iio a
⊢ map (fun (x : H) ↦ c * x) (𝓝[<] a) = 𝓝[<] (c * a)

Tactic:
convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.map_nhdsWithin_eq, Homeomorph.mulLeft
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Iio (c * a) = (⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Iio a

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Eq (α := Filter H) (map (⇑(Homeomorph.mulRight c) : (a : H) → H) (𝓝[>] a) : Filter H)
    (𝓝[(⇑(Homeomorph.mulRight c) : (a : H) → H) '' Ioi a] (Homeomorph.mulRight c : (a : H) → H) a : Filter H)

Tactic:
(Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq ..

Premises used: Homeomorph.isEmbedding, Homeomorph.mulRight, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
h : Ioi (a * c) = (⇑(Homeomorph.mulRight c) : (a : H) → H) '' Ioi a
⊢ map (fun (x : H) ↦ x * c) (𝓝[>] a) = 𝓝[>] (a * c)

Tactic:
convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Premises used: Homeomorph.isEmbedding, Homeomorph.mulRight, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Ioi (a * c) = (⇑(Homeomorph.mulRight c) : (a : H) → H) '' Ioi a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Eq (α := Filter H) (map (⇑(Homeomorph.mulRight c) : (a : H) → H) (𝓝[<] a) : Filter H)
    (𝓝[(⇑(Homeomorph.mulRight c) : (a : H) → H) '' Iio a] (Homeomorph.mulRight c : (a : H) → H) a : Filter H)

Tactic:
(Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq ..

Premises used: Homeomorph.isEmbedding, Homeomorph.mulRight, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
h : Iio (a * c) = (⇑(Homeomorph.mulRight c) : (a : H) → H) '' Iio a
⊢ map (fun (x : H) ↦ x * c) (𝓝[<] a) = 𝓝[<] (a * c)

Tactic:
convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Premises used: Homeomorph.isEmbedding, Homeomorph.mulRight, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ Iio (a * c) = (⇑(Homeomorph.mulRight c) : (a : H) → H) '' Iio a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Eq (α := Filter H) (map (⇑(Homeomorph.inv H) : (a : H) → H) (𝓝[>] a) : Filter H)
    (𝓝[(⇑(Homeomorph.inv H) : (a : H) → H) '' Ioi a] (Homeomorph.inv H : (a : H) → H) a : Filter H)

Tactic:
(Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq ..

Premises used: Homeomorph.isEmbedding, Homeomorph.inv, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
h : Iio a⁻¹ = (⇑(Homeomorph.inv H) : (a : H) → H) '' Ioi a
⊢ (𝓝[>] a)⁻¹ = 𝓝[<] a⁻¹

Tactic:
convert! (Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq .. using 2

Premises used: Homeomorph.isEmbedding, Homeomorph.inv, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Iio a⁻¹ = (⇑(Homeomorph.inv H) : (a : H) → H) '' Ioi a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Eq (α := Filter H) (map (⇑(Homeomorph.inv H) : (a : H) → H) (𝓝[<] a) : Filter H)
    (𝓝[(⇑(Homeomorph.inv H) : (a : H) → H) '' Iio a] (Homeomorph.inv H : (a : H) → H) a : Filter H)

Tactic:
(Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq ..

Premises used: Homeomorph.isEmbedding, Homeomorph.inv, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
h : Ioi a⁻¹ = (⇑(Homeomorph.inv H) : (a : H) → H) '' Iio a
⊢ (𝓝[<] a)⁻¹ = 𝓝[>] a⁻¹

Tactic:
convert! (Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq .. using 2

Premises used: Homeomorph.isEmbedding, Homeomorph.inv, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Ioi a⁻¹ = (⇑(Homeomorph.inv H) : (a : H) → H) '' Iio a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto (fun (a : H) ↦ a⁻¹) (𝓟 (Ioi a)) (𝓟 (Iio a⁻¹))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto (fun (a : H) ↦ a⁻¹) (𝓟 (Iio a)) (𝓟 (Ioi a⁻¹))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a)

Tactic:
simpa only [inv_inv] using tendsto_inv_nhdsGT (a := a⁻¹)

Premises used: inv_inv, tendsto_inv_nhdsGT
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)

Tactic:
simpa only [inv_inv] using tendsto_inv_nhdsLT (a := a⁻¹)

Premises used: inv_inv, tendsto_inv_nhdsLT
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto (fun (a : H) ↦ a⁻¹) (𝓟 (Ici a)) (𝓟 (Iic a⁻¹))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto (fun (a : H) ↦ a⁻¹) (𝓟 (Iic a)) (𝓟 (Ici a⁻¹))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a)

Tactic:
simpa only [inv_inv] using tendsto_inv_nhdsGE (a := a⁻¹)

Premises used: inv_inv, tendsto_inv_nhdsGE
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)

Tactic:
simpa only [inv_inv] using tendsto_inv_nhdsLE (a := a⁻¹)

Premises used: tendsto_inv_nhdsLE, inv_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
inst_4 : Inv α
inst_5 : ContinuousInv α
⊢ ContinuousInv.{u} αᵐᵒᵖ

Tactic:
opHomeomorph.symm.isInducing.continuousInv unop_inv

Premises used: Homeomorph.isInducing, MulOpposite.opHomeomorph, Homeomorph.symm, MulOpposite.unop_inv, Topology.IsInducing.continuousInv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ Eq.{w + 1} (α := Filter G) (comap Inv.inv (𝓝 1)) (𝓝 1)

Tactic:
((Homeomorph.inv G).comap_nhds_eq _).trans (congr_arg 𝓝 inv_one)

Premises used: inv_one, nhds, Homeomorph.comap_nhds_eq, Homeomorph.inv, congr_arg, Eq.trans
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ Eq.{w + 1} (α := Filter G) (map Inv.inv (𝓝 1)) (𝓝 1)

Tactic:
((Homeomorph.inv G).map_nhds_eq _).trans (congr_arg 𝓝 inv_one)

Premises used: inv_one, Homeomorph.map_nhds_eq, nhds, Homeomorph.inv, congr_arg, Eq.trans
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Set G
hS : Membership.mem (γ := Filter G) (𝓝 1) S
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hS : Membership.mem (γ := Filter G) (map Inv.inv (𝓝 1)) S), Membership.mem (γ := Filter G) (𝓝 1) S⁻¹
⊢ Membership.mem (γ := Filter G) (𝓝 1) S⁻¹

Tactic:
rwa [← nhds_one_symm'] at hS

Premises used: nhds_one_symm'
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ Eq (α := (a : G × G) → G × G) (⇑(Homeomorph.shearMulRight G) : (a : G × G) → G × G) fun (z : G × G) ↦ (z.1, z.1 * z.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ Eq (α := (a : G × G) → G × G) (⇑(Homeomorph.symm (Homeomorph.shearMulRight G)) : (a : G × G) → G × G)
    fun (z : G × G) ↦ (z.1, z.1⁻¹ * z.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : FunLike F H G
inst_6 : MonoidHomClass F H G
f : F
hf : IsInducing.{x, w} (X := H) (Y := G) (⇑f : (a : H) → G)
⊢ IsTopologicalGroup H

Tactic:
{ toContinuousMul := hf.continuousMul _
    toContinuousInv := hf.continuousInv (map_inv f) }

Premises used: Topology.IsInducing.continuousMul, map_inv, IsTopologicalGroup.mk, Topology.IsInducing.continuousInv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Type u_1
inst_3 : Group H
inst_4 : FunLike F H G
inst_5 : MonoidHomClass F H G
f : F
⊢ IsTopologicalGroup H

Tactic:
letI := induced f ‹_›
  IsInducing.topologicalGroup f ⟨rfl⟩

Premises used: Topology.IsInducing.mk, Topology.IsInducing.topologicalGroup, rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
S : Subgroup G
⊢ IsTopologicalGroup.{w} ↥S

Tactic:
IsInducing.subtypeVal.topologicalGroup S.subtype

Premises used: Subgroup.subtype, Topology.IsInducing.topologicalGroup, Topology.IsInducing.subtypeVal