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 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
rw :
  (∀ (x : G), 𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)) ↔
    Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
⊢ IsInducing.{w, u_1} (X := G) (Y := H) (⇑f : (a : G) → H) ↔
    Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))

Tactic:
rw [Topology.isInducing_iff_nhds]

Premises used: Topology.isInducing_iff_nhds
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
⊢ (∀ (x : G), 𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)) ↔
    Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))

Tactic:
⟨(map_one f ▸ · 1), fun hf x ↦ ?_⟩

Premises used: Eq.rec, map_one, Iff.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
refine :
  ∀ (hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))) (x : G),
    𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)
⊢ (∀ (x : G), 𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)) ↔
    Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))

Tactic:
refine ⟨(map_one f ▸ · 1), fun hf x ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
x : G
rw :
  Eq.{w + 1} (α := Filter G)
    (comap.{w, u_1} (β := H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
    (comap.{w, u_1} (β := H)
      ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H)) (𝓝 1))
⊢ 𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)

Tactic:
rw [← nhds_translation_mul_inv, ← nhds_translation_mul_inv (f x), Filter.comap_comap, hf,
    Filter.comap_comap]

Premises used: nhds_translation_mul_inv, Filter.comap_comap, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
x : G
e_m :
  Eq (α := G → H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹)
    ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H))
⊢ Eq.{w + 1} (α := Filter G)
    (comap.{w, u_1} (β := H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
    (comap.{w, u_1} (β := H)
      ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H)) (𝓝 1))

Tactic:
congr 1
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
x : G
e_m :
  ∀ (x_1 : G),
    Eq.{u_1 + 1} (α := H) (comp (β := G) (⇑f : (a : G) → H) (fun (x_2 : G) ↦ x_2 * x⁻¹) x_1)
      (((fun (x_2 : H) ↦ HMul.hMul (β := H) x_2 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H)) x_1)
⊢ Eq (α := G → H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹)
    ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
x x_1 : G
⊢ Eq.{u_1 + 1} (α := H) (comp (β := G) (⇑f : (a : G) → H) (fun (x_2 : G) ↦ x_2 * x⁻¹) x_1)
    (((fun (x_2 : H) ↦ HMul.hMul (β := H) x_2 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H)) x_1)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
⊢ IsOpenMap.{w, u_1} (X := G) (Y := H) (⇑f : (a : G) → H) ↔
    LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))

Tactic:
⟨fun H ↦ map_one f ▸ H.nhds_le 1, fun h ↦ IsOpenMap.of_nhds_le fun x ↦ ?_⟩

Premises used: Eq.rec, IsOpenMap.nhds_le, map_one, Iff.intro, IsOpenMap.of_nhds_le, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
refine :
  ∀ (h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))) (x : G),
    LE.le.{u_1} (α := Filter H) (𝓝 ((f : (a : G) → H) x) : Filter H) (map (⇑f : (a : G) → H) (𝓝 x) : Filter H)
⊢ IsOpenMap.{w, u_1} (X := G) (Y := H) (⇑f : (a : G) → H) ↔
    LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))

Tactic:
refine ⟨fun H ↦ map_one f ▸ H.nhds_le 1, fun h ↦ IsOpenMap.of_nhds_le fun x ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
⊢ Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)

Tactic:
simpa [-Homeomorph.map_nhds_eq, Units.smul_def] using
      (Homeomorph.smul ((toUnits x).map (MonoidHomClass.toMonoidHom f))).map_nhds_eq (1 : H)

Premises used: Homeomorph.map_nhds_eq, Homeomorph.smul, MonoidHomClass.toMonoidHom, Units.smul_def, toUnits, OfNat.ofNat, DFunLike.coe, Units.map
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
⊢ Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)

Tactic:
have : Filter.map (f x * ·) (𝓝 1) = 𝓝 (f x) := by
    simpa [-Homeomorph.map_nhds_eq, Units.smul_def] using
      (Homeomorph.smul ((toUnits x).map (MonoidHomClass.toMonoidHom f))).map_nhds_eq (1 : H)
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
this :
  Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)
rw :
  LE.le.{u_1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1))
    (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))
⊢ LE.le.{u_1} (α := Filter H) (𝓝 ((f : (a : G) → H) x) : Filter H) (map (⇑f : (a : G) → H) (𝓝 x) : Filter H)

Tactic:
rw [← map_mul_left_nhds_one x, Filter.map_map, Function.comp_def, ← this]

Premises used: Filter.map_map, Function.comp_def, map_mul_left_nhds_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
this :
  Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)
⊢ LE.le.{u_1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1))
    (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))

Tactic:
(Filter.map_mono h).trans ?_

Premises used: Filter.map_mono, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
this :
  Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)
refine :
  LE.le.{u_1} (α := Filter H)
    (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1)
      (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1)))
    (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))
⊢ LE.le.{u_1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1))
    (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))

Tactic:
refine (Filter.map_mono h).trans ?_

Premises used: Filter.map_mono, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
this :
  Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)
⊢ LE.le.{u_1} (α := Filter H)
    (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1)
      (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1)))
    (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
rw : IsOpen[inst_1] (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
⊢ IsOpen[inst_4] ((⇑φ : (a : A) → B) '' U)

Tactic:
rw [← hφ.isOpen_preimage]

Premises used: Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
this :
  Eq.{u_1 + 1} (α := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U)
k : A
h : k ∈ (↑(ker (↑φ : A →* B)) : Set A)
⊢ Continuous[inst_1, inst_1] fun (x : A) ↦ x * k

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
this :
  Eq.{u_1 + 1} (α := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U)
⊢ IsOpen[inst_1] (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))

Tactic:
exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
suffices :
  Eq.{u_1 + 1} (α := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U)
⊢ IsOpen[inst_1] (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))

Tactic:
suffices ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ ker (φ : A →* B), (fun x ↦ x * k) ⁻¹' U by
        exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
h :
  ∀ (x : A),
    Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x ↔
      Membership.mem (γ := Set A)
        (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
⊢ Eq.{u_1 + 1} (α := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x : A
h :
  Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x →
    Membership.mem (γ := Set A)
      (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
h₁ :
  Membership.mem (γ := Set A)
      (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x →
    Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x
⊢ Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x ↔
    Membership.mem (γ := Set A)
      (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x y : A
hyU : y ∈ U
hyx : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) y : B) ((φ : (a : A) → B) x : B)
h :
  Membership.mem (γ := Set A)
    (⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) (x⁻¹ * y)), (fun (x_1 : A) ↦ x_1 * (x⁻¹ * y)) ⁻¹' U) x
⊢ Membership.mem (γ := Set A)
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x

Tactic:
apply Set.mem_iUnion_of_mem (x⁻¹ * y)

Premises used: HMul.hMul, Inv.inv, Set.mem_iUnion_of_mem
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x y : A
hyU : y ∈ U
hyx : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) y : B) ((φ : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A)
    (⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) (x⁻¹ * y)), (fun (x_1 : A) ↦ x_1 * (x⁻¹ * y)) ⁻¹' U) x

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x k : A
hk : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) k : B) (1 : B)
hx :
  Membership.mem (γ := Set A)
    ((fun (h : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k) ↦ ((fun (x : A) ↦ x * k) ⁻¹' U : Set A)) hk) x
right : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) (x * k) : B) ((φ : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x

Tactic:
use x * k, hx
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x k : A
hk : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) k : B) (1 : B)
hx :
  Membership.mem (γ := Set A)
    ((fun (h : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k) ↦ ((fun (x : A) ↦ x * k) ⁻¹' U : Set A)) hk) x
right : HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) k : B) = (φ : (a : A) → B) x
right₁ : HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) x : B) (1 : B) = (φ : (a : A) → B) x
right₂ right₃ : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) x : B)
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) (x * k) : B) ((φ : (a : A) → B) x : B)

Tactic:
rw [map_mul, hk, mul_one]

Premises used: map_mul, mul_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (𝓝 1)
x : G
rw : comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1) = 𝓝 x
rw₁ :
  Eq.{u_1 + 1} (α := Filter G) (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
    (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := Filter G) (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
    (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
⊢ 𝓝 x = 𝓝 x

Tactic:
rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]

Premises used: nhds_translation_mul_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
⊢ t = t' ↔ Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (𝓝 1)

Tactic:
⟨fun h => h ▸ rfl, tg.ext tg'⟩

Premises used: Eq.rec, IsTopologicalGroup.ext, Iff.intro, rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
⊢ ContinuousInv G

Tactic:
⟨continuous_iff_continuousAt.2 fun x₀ => ?_⟩

Premises used: Iff.mpr, ContinuousInv.mk, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
refine : ∀ (x₀ : G), ContinuousAt (Y := G) (fun (a : G) ↦ a⁻¹) x₀
⊢ ContinuousInv G

Tactic:
refine ⟨continuous_iff_continuousAt.2 fun x₀ => ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
⊢ Tendsto (β := G) (fun (x : G) ↦ x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (fun (x : G) ↦ x₀⁻¹ * x) (𝓝 1))

Tactic:
have : Tendsto (fun x => x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (x₀⁻¹ * ·) (𝓝 1)) :=
    (tendsto_map.comp <| hconj x₀).comp hinv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
this : Tendsto (β := G) (fun (x : G) ↦ x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (fun (x : G) ↦ x₀⁻¹ * x) (𝓝 1))
⊢ ContinuousAt (Y := G) (fun (a : G) ↦ a⁻¹) x₀

Tactic:
simpa only [ContinuousAt, hleft x₀, hleft x₀⁻¹, tendsto_map'_iff, Function.comp_def, mul_assoc,
    mul_inv_rev, inv_mul_cancel_left] using this

Premises used: inv_mul_cancel_left, ContinuousAt, mul_assoc, Filter.tendsto_map'_iff, Function.comp_def, Inv.inv, mul_inv_rev
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
hmul :
  Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)
x₀ : G
rw : Eq.{u + 1} (α := Filter G) (map (α := G) ((fun (x : G) ↦ x * x₀⁻¹) ∘ fun (x : G) ↦ x * x₀) (𝓝 1)) (𝓝 1)
⊢ Eq.{u + 1} (α := Filter G) (map (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1)) (𝓝 1)

Tactic:
rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ←
              map_map, ← hleft, hright, map_map]

Premises used: Filter.map_map, rfl