awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
c a : G
⊢ Eq (α := Filter G) (map (⇑(Homeomorph.mulLeft c) : (a : G) → G) (𝓝[≠] a) : Filter G)
    (𝓝[image (α := G) (⇑(Homeomorph.mulLeft c) : (a : G) → G) {a}ᶜ] (Homeomorph.mulLeft c : (a : G) → G) a : Filter G)

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:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
c a : G
h : Eq (α := Set G) {c * a}ᶜ (image (α := G) (⇑(Homeomorph.mulLeft c) : (a : G) → G) {a}ᶜ)
⊢ map (fun (x : G) ↦ 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:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
c a : G
⊢ Eq (α := Set G) {c * a}ᶜ (image (α := G) (⇑(Homeomorph.mulLeft c) : (a : G) → G) {a}ᶜ)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ Eq (α := (a : G) → G) (⇑(Homeomorph.mulRight a) : (a : G) → G) fun (x : G) ↦ x * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
H :
  ∀ (x : G),
    Eq (α := G) ((Homeomorph.symm (Homeomorph.mulRight a) : (a : G) → G) x : G)
      ((Homeomorph.mulRight a⁻¹ : (a : G) → G) x : G)
⊢ Eq (α := G ≃ₜ G) (Homeomorph.symm (Homeomorph.mulRight a)) (Homeomorph.mulRight a⁻¹)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a x : G
⊢ Eq (α := G) ((Homeomorph.symm (Homeomorph.mulRight a) : (a : G) → G) x : G)
    ((Homeomorph.mulRight a⁻¹ : (a : G) → G) x : G)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ IsOpenMap (Y := G) fun (x : G) ↦ x * a

Tactic:
(Homeomorph.mulRight a).isOpenMap

Premises used: Homeomorph.mulRight, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
U : Set G
h : IsOpen[inst] U
x : G
⊢ IsOpen[inst] (op x • U)

Tactic:
isOpenMap_mul_right x _ h

Premises used: isOpenMap_mul_right, MulOpposite.unop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ IsClosedMap (Y := G) fun (x : G) ↦ x * a

Tactic:
(Homeomorph.mulRight a).isClosedMap

Premises used: Homeomorph.mulRight, Homeomorph.isClosedMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
U : Set G
h : IsClosed[inst] U
x : G
⊢ IsClosed[inst] (op x • U)

Tactic:
isClosedMap_mul_right x _ h

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

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:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
c a : G
h : Eq (α := Set G) {a * c}ᶜ (image (α := G) (⇑(Homeomorph.mulRight c) : (a : G) → G) {a}ᶜ)
⊢ map (fun (x : G) ↦ 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:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
c a : G
⊢ Eq (α := Set G) {a * c}ᶜ (image (α := G) (⇑(Homeomorph.mulRight c) : (a : G) → G) {a}ᶜ)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
⊢ DiscreteTopology G ↔ IsOpen[inst] {1}

Tactic:
MulAction.IsPretransitive.discreteTopology_iff G 1

Premises used: OfNat.ofNat, MulAction.IsPretransitive.discreteTopology_iff
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h : IsOpen[inst] {1}
⊢ DiscreteTopology G

Tactic:
discreteTopology_iff_isOpen_singleton_one.mpr h

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
g h : G
⊢ ∀ (y : G), IsConnected (α := G) (preimage (β := G) (⇑(Homeomorph.mulLeft g) : (a : G) → G) {y})

Tactic:
simp [isConnected_singleton]

Premises used: isConnected_singleton
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h : Eq (α := Set G) (connectedComponent 1) {1}
g : G
rw : connectedComponent (g * 1) = {g * 1}
rw₁ : HSMul.hSMul (β := Set G) g (connectedComponent 1) = {g * 1}
rw₂ : HSMul.hSMul (β := Set G) g {1} = {g * 1}
rw₃ : Eq (α := Set G) {HSMul.hSMul (β := G) g 1} {g * 1}
rw₄ rw₅ : Eq (α := Set G) {g * 1} {g * 1}
⊢ connectedComponent g = {g}

Tactic:
rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_mul]

Premises used: smul_connectedComponent, Set.smul_set_singleton, smul_eq_mul, mul_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) ↔ Tendsto f l (𝓝 c)

Tactic:
⟨?_, Tendsto.mul_const b⟩

Premises used: Filter.Tendsto.mul_const, Iff.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
refine : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → Tendsto f l (𝓝 c)
⊢ Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨?_, Tendsto.mul_const b⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ ∀ (hf : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b))), Tendsto (fun (x : α) ↦ f x * b * b⁻¹) l (𝓝 (c * b * b⁻¹))

Tactic:
Tendsto.mul_const b⁻¹

Premises used: Filter.Tendsto.mul_const, Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → ∀ (x : α), f x = f x * b * b⁻¹
h₁ : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → c = c * b * b⁻¹
⊢ Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → Tendsto f l (𝓝 c)

Tactic:
convert! Tendsto.mul_const b⁻¹ using 3

Premises used: Filter.Tendsto.mul_const, Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h_1 : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b))
x : α
h h₁ : f x = f x
⊢ f x = f x * b * b⁻¹

Tactic:
rw [mul_inv_cancel_right]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h_1 : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b))
h h₁ : c = c
⊢ c = c * b * b⁻¹

Tactic:
rw [mul_inv_cancel_right]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) ↔ Tendsto f l (𝓝 c)

Tactic:
⟨?_, Tendsto.const_mul b⟩

Premises used: Filter.Tendsto.const_mul, Iff.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
refine : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → Tendsto f l (𝓝 c)
⊢ Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨?_, Tendsto.const_mul b⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ ∀ (hf : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c))), Tendsto (fun (x : α) ↦ b⁻¹ * (b * f x)) l (𝓝 (b⁻¹ * (b * c)))

Tactic:
Tendsto.const_mul b⁻¹

Premises used: Filter.Tendsto.const_mul, Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → ∀ (x : α), f x = b⁻¹ * (b * f x)
h₁ : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → c = b⁻¹ * (b * c)
⊢ Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → Tendsto f l (𝓝 c)

Tactic:
convert! Tendsto.const_mul b⁻¹ using 3

Premises used: Filter.Tendsto.const_mul, Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h_1 : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c))
x : α
h h₁ : f x = f x
⊢ f x = b⁻¹ * (b * f x)

Tactic:
rw [inv_mul_cancel_left]

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h_1 : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c))
h h₁ : c = c
⊢ c = b⁻¹ * (b * c)

Tactic:
rw [inv_mul_cancel_left]

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike F α β
inst_1 : Group α
inst_2 : DivisionMonoid β
inst_3 : MonoidHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ ContinuousInv α

Tactic:
⟨continuous_induced_rng.2 ?_⟩

Premises used: Iff.mpr, ContinuousInv.mk, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike F α β
inst_1 : Group α
inst_2 : DivisionMonoid β
inst_3 : MonoidHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
refine :
  Continuous[TopologicalSpace.induced (⇑f : (a : α) → β) tβ, tβ] (comp (β := α) (⇑f : (a : α) → β) fun (a : α) ↦ a⁻¹)
⊢ ContinuousInv α

Tactic:
refine ⟨continuous_induced_rng.2 ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike F α β
inst_1 : Group α
inst_2 : DivisionMonoid β
inst_3 : MonoidHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
simp : Continuous[TopologicalSpace.induced (⇑f : (a : α) → β) tβ, tβ] fun (x : α) ↦ ((f : (a : α) → β) x)⁻¹
⊢ Continuous[TopologicalSpace.induced (⇑f : (a : α) → β) tβ, tβ] (comp (β := α) (⇑f : (a : α) → β) fun (a : α) ↦ a⁻¹)

Tactic:
simp only [Function.comp_def, map_inv]

Premises used: map_inv, Function.comp_def
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike F α β
inst_1 : Group α
inst_2 : DivisionMonoid β
inst_3 : MonoidHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ Continuous[TopologicalSpace.induced (⇑f : (a : α) → β) tβ, tβ] fun (x : α) ↦ ((f : (a : α) → β) x)⁻¹

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
x y : G
h : x ⤳ y
⊢ x⁻¹ ⤳ y⁻¹

Tactic:
h.map continuous_inv

Premises used: Specializes.map, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
x y : G
h : Inseparable x y
⊢ Inseparable x⁻¹ y⁻¹

Tactic:
h.map continuous_inv

Premises used: ContinuousInv.continuous_inv, Inseparable.map
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
inst_2 : ContinuousMul G
inst_3 : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.ofNat n) ⤳ (y ^ Int.ofNat n)

Tactic:
simpa using h.pow n

Premises used: Specializes.pow
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
inst_2 : ContinuousMul G
inst_3 : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.negSucc n) ⤳ (y ^ Int.negSucc n)

Tactic:
simpa using (h.pow (n + 1)).inv

Premises used: HAdd.hAdd, Specializes.inv, OfNat.ofNat, Specializes.pow
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
inst_2 : ContinuousMul G
inst_3 : ContinuousInv G
x y : G
h : Inseparable x y
m : ℤ
⊢ Inseparable (x ^ m) (y ^ m)

Tactic:
(h.specializes.zpow m).antisymm (h.specializes'.zpow m)

Premises used: Inseparable.specializes', Specializes.zpow, Specializes.antisymm, Inseparable.specializes
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
⊢ ContinuousInv (ULift.{u_1, w} G)

Tactic:
⟨continuous_uliftUp.comp (continuous_inv.comp continuous_uliftDown)⟩

Premises used: ContinuousInv.mk, Continuous.comp, continuous_uliftUp, continuous_uliftDown, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
s : Set G
⊢ ContinuousOn Inv.inv s

Tactic:
continuous_inv.continuousOn

Premises used: Continuous.continuousOn, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
s : Set G
x : G
⊢ ContinuousWithinAt Inv.inv s x

Tactic:
continuous_inv.continuousWithinAt

Premises used: Continuous.continuousWithinAt, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
x : G
⊢ ContinuousAt Inv.inv x

Tactic:
continuous_inv.continuousAt

Premises used: Continuous.continuousAt, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
a : G
⊢ Tendsto Inv.inv (𝓝 a) (𝓝 a⁻¹)

Tactic:
continuousAt_inv

Premises used: ContinuousAt, continuousAt_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
inst_4 : TopologicalSpace H
inst_5 : Inv H
inst_6 : ContinuousInv H
⊢ ContinuousInv (G × H)

Tactic:
⟨continuous_inv.fst'.prodMk continuous_inv.snd'⟩

Premises used: ContinuousInv.mk, Continuous.fst', Continuous.snd', ContinuousInv.continuous_inv, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
⊢ ContinuousInv (ι → G)

Tactic:
Pi.continuousInv

Premises used: Pi.continuousInv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
inst_4 : TopologicalSpace H
inst_5 : Inv H
inst_6 : DiscreteTopology H
⊢ ContinuousInv H

Tactic:
⟨continuous_of_discreteTopology⟩

Premises used: ContinuousInv.mk, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
inst_4 : TopologicalSpace H
inst_5 : Inv H
inst_6 : IndiscreteTopology H
⊢ ContinuousInv H

Tactic:
⟨continuous_of_indiscreteTopology⟩

Premises used: ContinuousInv.mk, continuous_of_indiscreteTopology
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
inst_4 : TopologicalSpace H
inst_5 : Div H
inst_6 : DiscreteTopology H
⊢ ContinuousDiv H

Tactic:
⟨continuous_of_discreteTopology⟩

Premises used: ContinuousDiv.mk, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
inst_4 : TopologicalSpace H
inst_5 : Div H
inst_6 : IndiscreteTopology H
⊢ ContinuousDiv H

Tactic:
⟨continuous_of_indiscreteTopology⟩

Premises used: ContinuousDiv.mk, continuous_of_indiscreteTopology
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
inst_4 : TopologicalSpace H
inst_5 : Group H
inst_6 : DiscreteTopology H
⊢ IsTopologicalGroup H

Tactic:
⟨⟩

Premises used: IsTopologicalGroup.mk
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
inst_3 : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
inst_4 : TopologicalSpace H
inst_5 : Group H
inst_6 : IndiscreteTopology H
⊢ IsTopologicalGroup H

Tactic:
⟨⟩

Premises used: IsTopologicalGroup.mk
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : TopologicalSpace G₂
inst_1 : T2Space G₂
inst_2 : Inv G₁
inst_3 : Inv G₂
inst_4 : ContinuousInv G₂
simp : IsClosed[Pi.topologicalSpace] (⋂ (i : G₁), {x : G₁ → G₂ | x i⁻¹ = (x i)⁻¹})
⊢ IsClosed[Pi.topologicalSpace] {f : G₁ → G₂ | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

Tactic:
simp only [setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : TopologicalSpace G₂
inst_1 : T2Space G₂
inst_2 : Inv G₁
inst_3 : Inv G₂
inst_4 : ContinuousInv G₂
⊢ IsClosed[Pi.topologicalSpace] (⋂ (i : G₁), {x : G₁ → G₂ | x i⁻¹ = (x i)⁻¹})

Tactic:
isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv

Premises used: isClosed_eq, isClosed_iInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : TopologicalSpace G₂
inst_1 : T2Space G₂
inst_2 : Inv G₁
inst_3 : Inv G₂
inst_4 : ContinuousInv G₂
⊢ IsClosed[Pi.topologicalSpace] (⋂ (i : G₁), {x : G₁ → G₂ | x i⁻¹ = (x i)⁻¹})

Tactic:
exact isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv

Premises used: isClosed_eq, continuous_apply, Continuous.inv, isClosed_iInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
l : Filter α
m : α → G
a : G
h : Tendsto (fun (x : α) ↦ (m x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto m l (𝓝 a)

Tactic:
simpa only [inv_inv] using h.inv

Premises used: Filter.Tendsto.inv, inv_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
s : Set G
hs : IsCompact s
rw : IsCompact (X := G) ((fun (x : G) ↦ x⁻¹) '' s)
⊢ IsCompact s⁻¹

Tactic:
rw [← image_inv_eq_inv]

Premises used: Set.image_inv_eq_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact (X := G) ((fun (x : G) ↦ x⁻¹) '' s)

Tactic:
hs.image continuous_inv

Premises used: ContinuousInv.continuous_inv, IsCompact.image
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact (X := G) ((fun (x : G) ↦ x⁻¹) '' s)

Tactic:
exact hs.image continuous_inv

Premises used: ContinuousInv.continuous_inv, IsCompact.image
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
⊢ Eq (α := G ≃ₜ G) (Homeomorph.symm (Homeomorph.inv G)) (Homeomorph.inv G)

Tactic:
rfl

Premises used: Equiv.inv, Function.Involutive.toPerm, Homeomorph.inv, Homeomorph.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
⊢ Eq (α := (a : G) → G) (⇑(Homeomorph.inv G) : (a : G) → G) Inv.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
a : G
⊢ 𝓝 a⁻¹ = (𝓝 a)⁻¹

Tactic:
((Homeomorph.inv G).map_nhds_eq a).symm

Premises used: Homeomorph.map_nhds_eq, Homeomorph.inv, Eq.symm
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
⊢ IsOpenMap.{w, w} (X := G) Inv.inv

Tactic:
(Homeomorph.inv _).isOpenMap

Premises used: Homeomorph.inv, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
⊢ IsClosedMap.{w, w} (X := G) Inv.inv

Tactic:
(Homeomorph.inv _).isClosedMap

Premises used: Homeomorph.inv, Homeomorph.isClosedMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
s : Set G
hs : IsOpen[inst] s
⊢ IsOpen[inst] s⁻¹

Tactic:
hs.preimage continuous_inv

Premises used: IsOpen.preimage, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
s : Set G
hs : IsClosed[inst] s
⊢ IsClosed[inst] s⁻¹

Tactic:
hs.preimage continuous_inv

Premises used: IsClosed.preimage, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
⊢ ∀ (s : Set G), (closure[inst] s)⁻¹ = closure[inst] s⁻¹

Tactic:
(Homeomorph.inv G).preimage_closure

Premises used: Homeomorph.inv, Homeomorph.preimage_closure
-- 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
⊢ Continuous[inst_3, inst] f⁻¹ ↔ Continuous[inst_3, inst] f

Tactic:
(Homeomorph.inv G).comp_continuous_iff

Premises used: Homeomorph.comp_continuous_iff, Homeomorph.inv