awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : Membership.mem (γ := Filter Gᵐᵒᵖ) (𝓝 (op 1)) V
hV' : op '' K * V ⊆ op '' U
rwa : ∀ (hV' : op '' K * op '' op ⁻¹' V ⊆ op '' U), op ⁻¹' V * K ⊆ U
rwa₁ : ∀ (hV' : op '' (op ⁻¹' V * K) ⊆ op '' U), op ⁻¹' V * K ⊆ U
rwa₂ : ∀ (hV' : op ⁻¹' V * K ⊆ op ⁻¹' op '' U), op ⁻¹' V * K ⊆ U
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hV' : op ⁻¹' V * K ⊆ U), op ⁻¹' V * K ⊆ U
⊢ op ⁻¹' V * K ⊆ U

Tactic:
rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff,
    preimage_image_eq _ op_injective] at hV'

Premises used: MulOpposite.op_injective, Set.image_preimage_eq, Set.preimage_image_eq, Set.image_subset_iff, MulOpposite.op_surjective, Set.image_op_mul
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ (t : Finset G), K ⊆ ⋃ x ∈ t, interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V)

Tactic:
hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_

Premises used: HMul.hMul, isOpen_interior, IsCompact.elim_finite_subcover, Set.preimage, interior
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
x : K ⊆ ⋃ (i : G), (fun (x : G) ↦ (interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V) : Set G)) i
⊢ ∃ (t : Finset G), K ⊆ ⋃ x ∈ t, interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V)

Tactic:
refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_

Premises used: HMul.hMul, isOpen_interior, IsCompact.elim_finite_subcover, Set.preimage, interior
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
obtain :
  ∀ (g₀ : G) (hg₀ : g₀ ∈ interior V),
    K ⊆ ⋃ (i : G), (fun (x : G) ↦ (interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V) : Set G)) i
⊢ K ⊆ ⋃ (i : G), (fun (x : G) ↦ (interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V) : Set G)) i

Tactic:
obtain ⟨g₀, hg₀⟩ := hV
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
⊢ K ⊆ ⋃ (i : G), (fun (x : G) ↦ (interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V) : Set G)) i

Tactic:
fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Set.Mem, Set.mem_iUnion, Set.Subset, Inv.inv, Exists.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
refine : ∀ g ∈ K, Membership.mem (γ := Set G) (interior ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' V)) g
⊢ K ⊆ ⋃ (i : G), (fun (x : G) ↦ (interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V) : Set G)) i

Tactic:
refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Set.mem_iUnion, Inv.inv, Exists.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
h : g ∈ K
⊢ Continuous[inst, inst] fun (x : G) ↦ g₀ * g⁻¹ * x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
h : g ∈ K
refine : Membership.mem (γ := Set G) ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' interior V) g
⊢ Membership.mem (γ := Set G) (interior ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' V)) g

Tactic:
refine preimage_interior_subset_interior_preimage (by fun_prop) ?_

Premises used: preimage_interior_subset_interior_preimage
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
h : g ∈ K
rwa : g₀ * g⁻¹ * g ∈ interior V
rwa₁ rwa₂ rwa₃ rwa₄ : g₀ ∈ interior V
⊢ Membership.mem (γ := Set G) ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' interior V) g

Tactic:
rwa [mem_preimage, inv_mul_cancel_right]

Premises used: inv_mul_cancel_right, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
obtain :
  ∀ (t : Finset G) (ht : K ⊆ ⋃ x ∈ t, interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V)),
    ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V
⊢ ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V

Tactic:
obtain ⟨t, ht⟩ : ∃ t : Finset G, K ⊆ ⋃ x ∈ t, interior ((x * ·) ⁻¹' V) := by
    refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_
    obtain ⟨g₀, hg₀⟩ := hV
    refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩
    refine preimage_interior_subset_interior_preimage (by fun_prop) ?_
    rwa [mem_preimage, inv_mul_cancel_right]

Premises used: Finset
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ x ∈ t, interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V)
⊢ ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V

Tactic:
⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩

Premises used: interior_subset, Set.Subset.trans, Set.iUnion₂_mono, Exists.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ x ∈ t, interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V)
⊢ ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V

Tactic:
exact ⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
obtain : ∀ (L : Set G) (hLc : IsCompact L) (hL1 : Membership.mem (γ := Filter G) (𝓝 1) L), SigmaCompactSpace G
⊢ SigmaCompactSpace G

Tactic:
obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G)

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, OfNat.ofNat
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
⊢ SigmaCompactSpace G

Tactic:
⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, ?_, ?_⟩⟩

Premises used: HMul.hMul, SigmaCompactSpace.mk, Set.preimage, And.intro, Exists.intro, TopologicalSpace.denseSeq
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
refine_1 : ∀ (n : ℕ), IsCompact.{w} (X := G) ((fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n)
refine_2 : Eq.{w + 1} (α := Set G) (⋃ (n : ℕ), (fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n) univ
⊢ SigmaCompactSpace G

Tactic:
refine ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, ?_, ?_⟩⟩
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
n : ℕ
⊢ IsCompact.{w} (X := G) ((fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n)

Tactic:
(Homeomorph.mulRight _).isCompact_preimage.mpr hLc

Premises used: Iff.mpr, Homeomorph.mulRight, Homeomorph.isCompact_preimage, Classical.choose, TopologicalSpace.denseSeq
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
n : ℕ
⊢ IsCompact.{w} (X := G) ((fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n)

Tactic:
exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc

Premises used: Iff.mpr, Homeomorph.mulRight, Homeomorph.isCompact_preimage
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
⊢ Eq.{w + 1} (α := Set G) (⋃ (n : ℕ), (fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n) univ

Tactic:
iUnion_eq_univ_iff.2 fun x => ?_

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
refine_2 : ∀ (x : G), ∃ (i : ℕ), Membership.mem (γ := Set G) ((fun (x : G) ↦ x * denseSeq G i) ⁻¹' L) x
⊢ Eq.{w + 1} (α := Set G) (⋃ (n : ℕ), (fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n) univ

Tactic:
refine iUnion_eq_univ_iff.2 fun x => ?_

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
x : G
⊢ Membership.mem (γ := Filter G)
    (𝓝 ((Homeomorph.mulLeft x : (a : G) → G) ((Homeomorph.symm (Homeomorph.mulLeft x) : (a : G) → G) 1 : G)) : Filter G)
    L

Tactic:
rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1

Premises used: Homeomorph.mulLeft, Homeomorph.apply_symm_apply, OfNat.ofNat
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
x : G
hL1 :
  Membership.mem (γ := Filter G)
    (𝓝 ((Homeomorph.mulLeft x : (a : G) → G) ((Homeomorph.symm (Homeomorph.mulLeft x) : (a : G) → G) 1 : G)) : Filter G)
    L
⊢ (range (denseSeq G) ∩ (fun (y : G) ↦ x * y) ⁻¹' L).Nonempty

Tactic:
(denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)

Premises used: TopologicalSpace.denseRange_denseSeq, Homeomorph.continuous, Continuous.continuousAt, Dense.inter_nhds_nonempty, Homeomorph.mulLeft
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
x : G
hL1 :
  Membership.mem (γ := Filter G)
    (𝓝 ((Homeomorph.mulLeft x : (a : G) → G) ((Homeomorph.symm (Homeomorph.mulLeft x) : (a : G) → G) 1 : G)) : Filter G)
    L
⊢ (range (denseSeq G) ∩ (fun (y : G) ↦ x * y) ⁻¹' L).Nonempty

Tactic:
exact (denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)

Premises used: TopologicalSpace.denseRange_denseSeq, Homeomorph.continuous, Continuous.continuousAt, Dense.inter_nhds_nonempty, Homeomorph.mulLeft
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
x : G
refine_2 :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Set G) ((fun (y : G) ↦ x * y) ⁻¹' L) (denseSeq G n)),
    ∃ (i : ℕ), Membership.mem (γ := Set G) ((fun (x : G) ↦ x * denseSeq G i) ⁻¹' L) x
⊢ ∃ (i : ℕ), Membership.mem (γ := Set G) ((fun (x : G) ↦ x * denseSeq G i) ⁻¹' L) x

Tactic:
obtain ⟨_, ⟨n, rfl⟩, hn⟩ : (range (denseSeq G) ∩ (fun y => x * y) ⁻¹' L).Nonempty := by
      rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
      exact (denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)

Premises used: HMul.hMul, Inter.inter, Set.Nonempty, Set.preimage, Set.range, TopologicalSpace.denseSeq, 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
x : G
n : ℕ
hn : Membership.mem (γ := Set G) ((fun (y : G) ↦ x * y) ⁻¹' L) (denseSeq G n)
⊢ ∃ (i : ℕ), Membership.mem (γ := Set G) ((fun (x : G) ↦ x * denseSeq G i) ⁻¹' L) x

Tactic:
⟨n, hn⟩

Premises used: Exists.intro
-- 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 : SeparableSpace G
inst_4 : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : Membership.mem (γ := Filter G) (𝓝 1) L
x : G
n : ℕ
hn : Membership.mem (γ := Set G) ((fun (y : G) ↦ x * y) ⁻¹' L) (denseSeq G n)
⊢ ∃ (i : ℕ), Membership.mem (γ := Set G) ((fun (x : G) ↦ x * denseSeq G i) ⁻¹' L) x

Tactic:
exact ⟨n, hn⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ ¬K * L⁻¹ = univ

Tactic:
have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
contrapose! : ∀ (A : ∀ (g : G), g ∈ K * L⁻¹), K * L⁻¹ = univ
⊢ ∃ (g : G), g ∉ K * L⁻¹

Tactic:
contrapose! A
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ∀ (g : G), g ∈ K * L⁻¹
⊢ K * L⁻¹ = univ

Tactic:
eq_univ_iff_forall.2 A

Premises used: Iff.mpr, Set.eq_univ_iff_forall
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ∀ (g : G), g ∈ K * L⁻¹
⊢ K * L⁻¹ = univ

Tactic:
exact eq_univ_iff_forall.2 A

Premises used: Iff.mpr, Set.eq_univ_iff_forall
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
obtain : ∀ (g : G) (hg : g ∉ K * L⁻¹), ∃ (g : G), Disjoint K (g • L)
⊢ ∃ (g : G), Disjoint K (g • L)

Tactic:
obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
    contrapose! A
    exact eq_univ_iff_forall.2 A
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
⊢ ∃ (g : G), Disjoint K (g • L)

Tactic:
⟨g, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
refine : Disjoint K (g • L)
⊢ ∃ (g : G), Disjoint K (g • L)

Tactic:
refine ⟨g, ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
⊢ Disjoint K (g • L)

Tactic:
disjoint_left.2 fun a ha h'a => hg ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
refine : ∀ (a : G) (ha : a ∈ K) (h'a : a ∈ g • L), g ∈ K * L⁻¹
⊢ Disjoint K (g • L)

Tactic:
refine disjoint_left.2 fun a ha h'a => hg ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
a : G
ha : a ∈ K
h'a : a ∈ g • L
rcases : ∀ (b : G) (bL : b ∈ L) (ha : (fun (x : G) ↦ g • x) b ∈ K), g ∈ K * L⁻¹
⊢ g ∈ K * L⁻¹

Tactic:
rcases h'a with ⟨b, bL, 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
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun (x : G) ↦ g • x) b ∈ K
⊢ b⁻¹ ∈ L⁻¹

Tactic:
simpa only [Set.mem_inv, inv_inv] using bL

Premises used: inv_inv, Set.mem_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun (x : G) ↦ g • x) b ∈ K
refine : (fun (x1 x2 : G) ↦ x1 * x2) (g * b) b⁻¹ = g
⊢ g ∈ K * L⁻¹

Tactic:
refine ⟨g * b, ha, b⁻¹, by simpa only [Set.mem_inv, inv_inv] using bL, ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun (x : G) ↦ g • x) b ∈ K
⊢ (fun (x1 x2 : G) ↦ x1 * x2) (g * b) b⁻¹ = g

Tactic:
simp only [mul_inv_cancel_right]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
⊢ 𝓝 (x * y) = map (fun (x_1 : G) ↦ x * x_1) (map (fun (x : G) ↦ x * y) (HMul.hMul (α := Filter G) (𝓝 1) (𝓝 1)))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
rw :
  Eq.{w + 1} (α := Filter G)
    (map (fun (x_1 : G) ↦ x * x_1) (map (fun (x : G) ↦ x * y) (map₂ (fun (x1 x2 : G) ↦ x1 * x2) (𝓝 1) (𝓝 1))))
    (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
rw₁ :
  Eq.{w + 1} (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (map₂ (fun (a b : G) ↦ a * b * y) (𝓝 1) (𝓝 1)))
    (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
rw₂ rw₃ :
  Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
⊢ Eq (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (map (fun (x : G) ↦ x * y) (HMul.hMul (α := Filter G) (𝓝 1) (𝓝 1))))
    (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))

Tactic:
rw [← map₂_mul, map_map₂, map_map₂]

Premises used: Filter.map₂_mul, Filter.map_map₂
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
⊢ Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
rw : map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map (fun (x_1 : G) ↦ x * x_1) (𝓝 1) * 𝓝 y
rw₁ :
  map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) =
    HMul.hMul (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1))
rw₂ :
  Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (x1 x2 : G) ↦ x1 * x2) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1)))
rw₃ :
  Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (a b : G) ↦ x * a * b) (𝓝 1) (map (fun (x : G) ↦ x * y) (𝓝 1)))
rw₄ rw₅ :
  Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
⊢ map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y

Tactic:
rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
        map₂_map_right]

Premises used: map_mul_right_nhds_one, Filter.map₂_map_right, Filter.map₂_map_left, Filter.map₂_mul, map_mul_left_nhds_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
⊢ IsEmbedding.{w, w} (X := Gˣ) val

Tactic:
toUnits_homeomorph.symm.isEmbedding

Premises used: Homeomorph.isEmbedding, toUnits_homeomorph, Homeomorph.symm
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : Group G
inst_1 : Monoid H
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace H
inst_4 : ContinuousInv G
f : MonoidHom.{w, x} G Hˣ
hf : Continuous[inst_2, inst_3] (⇑(MonoidHom.comp (Units.coeHom H) f) : (a : G) → H)
apply :
  Continuous[inst_2, inferInstance]
    (Function.comp (β := Hˣ) (⇑(Units.embedProduct H) : (a : Hˣ) → H × Hᵐᵒᵖ) (⇑f : (a : G) → Hˣ))
⊢ Continuous[inst_2, Units.instTopologicalSpaceUnits] (⇑f : (a : G) → Hˣ)

Tactic:
apply continuous_induced_rng.mpr ?_

Premises used: Iff.mpr, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : Group G
inst_1 : Monoid H
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace H
inst_4 : ContinuousInv G
f : MonoidHom.{w, x} G Hˣ
hf : Continuous[inst_2, inst_3] (⇑(MonoidHom.comp (Units.coeHom H) f) : (a : G) → H)
⊢ Continuous[inst_2, inferInstance]
    (Function.comp (β := Hˣ) (⇑(Units.embedProduct H) : (a : Hˣ) → H × Hᵐᵒᵖ) (⇑f : (a : G) → Hˣ))

Tactic:
continuous_prodMk.mpr ⟨hf, ?_⟩

Premises used: Iff.mpr, And.intro, continuous_prodMk
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : Group G
inst_1 : Monoid H
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace H
inst_4 : ContinuousInv G
f : MonoidHom.{w, x} G Hˣ
hf : Continuous[inst_2, inst_3] (⇑(MonoidHom.comp (Units.coeHom H) f) : (a : G) → H)
refine : Continuous[inst_2, instTopologicalSpaceMulOpposite] fun (x : G) ↦ op (↑((f : (a : G) → Hˣ) x)⁻¹ : H)
⊢ Continuous[inst_2, inferInstance]
    (Function.comp (β := Hˣ) (⇑(Units.embedProduct H) : (a : Hˣ) → H × Hᵐᵒᵖ) (⇑f : (a : G) → Hˣ))

Tactic:
refine continuous_prodMk.mpr ⟨hf, ?_⟩

Premises used: Iff.mpr, And.intro, continuous_prodMk