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 : ContinuousMul G
h : IsClosed[inst] {1}
x : G
⊢ IsClosed[inst] {x}

Tactic:
simpa using isClosedMap_mul_right x _ h

Premises used: isClosedMap_mul_right
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ

Tactic:
have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ
⊢ Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))

Tactic:
rw [preimage_compl, compl_compl] at H

Premises used: compl_compl, Set.preimage_compl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
⊢ Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))

Tactic:
H
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
h :
  Eq (α := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
    (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
⊢ Set.Finite.{w} (α := ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}

Tactic:
convert! H
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
h :
  ∀ (x : ↥S),
    Membership.mem (γ := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty} x ↔
      Membership.mem (γ := Set ↥S)
        (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)) x
⊢ Eq (α := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
    (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
x : ↥S
h : (x • K ∩ L).Nonempty ↔ ∃ (a : G) (b : G), (a, b) ∈ L ×ˢ K ∧ a / b = (↑x : G)
⊢ Membership.mem (γ := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty} x ↔
    Membership.mem (γ := Set ↥S)
      (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)) x

Tactic:
simp only [image_smul, mem_setOf_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]

Premises used: Set.image_smul, Subgroup.coe_subtype, Set.mem_image, Set.mem_setOf_eq, Prod.exists, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
x : ↥S
⊢ (x • K ∩ L).Nonempty ↔ ∃ (a : G) (b : G), (a, b) ∈ L ×ˢ K ∧ a / b = (↑x : G)

Tactic:
Set.smul_inter_nonempty_iff'

Premises used: Set.Mem, setOf, Set.prod, Set.smul_inter_nonempty_iff'
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
x : ↥S
⊢ (x • K ∩ L).Nonempty ↔ ∃ (a : G) (b : G), (a, b) ∈ L ×ˢ K ∧ a / b = (↑x : G)

Tactic:
exact Set.smul_inter_nonempty_iff'

Premises used: Set.smul_inter_nonempty_iff'
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)

Tactic:
have : Continuous fun p : G × G => (p.1⁻¹, p.2) := continuous_inv.prodMap continuous_id
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
⊢ Set.Finite (α := ↥S)
    (preimage (β := G) (⇑S.subtype : (a : ↥S) → G)
        (((fun (p : G × G) ↦ p.1 * p.2) ∘ fun (p : G × G) ↦ (p.1⁻¹, p.2)) '' K ×ˢ L)ᶜ)ᶜ

Tactic:
have H : Set.Finite _ :=
        hS ((hK.prod hL).image (continuous_mul.comp this)).compl_mem_cocompact
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H :
  Set.Finite (α := ↥S)
    (preimage (β := G) (⇑S.subtype : (a : ↥S) → G)
        (((fun (p : G × G) ↦ p.1 * p.2) ∘ fun (p : G × G) ↦ (p.1⁻¹, p.2)) '' K ×ˢ L)ᶜ)ᶜ
⊢ Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)

Tactic:
simp only [preimage_compl, compl_compl, coe_subtype, comp_apply] at H

Premises used: compl_compl, Subgroup.coe_subtype, Function.comp_apply, Set.preimage_compl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
apply :
  Set.Finite (α := ↥S)
    (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})
⊢ Set.Finite.{w} (α := ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}

Tactic:
apply Finite.of_preimage _ (equivOp S).surjective

Premises used: Subgroup.equivOp, Set.Finite.of_preimage, Equiv.surjective
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
⊢ Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)

Tactic:
H
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
h :
  Eq (α := Set ↥S)
    (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})
    (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
⊢ Set.Finite (α := ↥S)
    (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})

Tactic:
convert! H using 1
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
h :
  ∀ (x : ↥S),
    Membership.mem (γ := Set ↥S)
        (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})
        x ↔
      Membership.mem (γ := Set ↥S)
        (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L) x
⊢ Eq (α := Set ↥S)
    (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})
    (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
x : ↥S
h :
  (HSMul.hSMul (α := ↥S.op) ((S.equivOp : (a : ↥S) → ↥S.op) x : ↥S.op) K ∩ L).Nonempty ↔
    ∃ (a : G) (b : G), (a, b) ∈ K ×ˢ L ∧ a⁻¹ * b = (↑x : G)
⊢ Membership.mem (γ := Set ↥S)
      (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})
      x ↔
    Membership.mem (γ := Set ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
      x

Tactic:
simp only [image_smul, mem_setOf_eq, mem_preimage, mem_image, Prod.exists]

Premises used: Set.image_smul, Set.mem_image, Set.mem_setOf_eq, Prod.exists, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
x : ↥S
⊢ (HSMul.hSMul (α := ↥S.op) ((S.equivOp : (a : ↥S) → ↥S.op) x : ↥S.op) K ∩ L).Nonempty ↔
    ∃ (a : G) (b : G), (a, b) ∈ K ×ˢ L ∧ a⁻¹ * b = (↑x : G)

Tactic:
Set.op_smul_inter_nonempty_iff

Premises used: Set.Mem, setOf, Set.prod, Set.op_smul_inter_nonempty_iff, MulOpposite.unop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
x : ↥S
⊢ (HSMul.hSMul (α := ↥S.op) ((S.equivOp : (a : ↥S) → ↥S.op) x : ↥S.op) K ∩ L).Nonempty ↔
    ∃ (a : G) (b : G), (a, b) ∈ K ×ˢ L ∧ a⁻¹ * b = (↑x : G)

Tactic:
exact Set.op_smul_inter_nonempty_iff

Premises used: Set.op_smul_inter_nonempty_iff
-- 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), Membership.mem (γ := Filter G) (𝓝 1) V ∧ K * V ⊆ U

Tactic:
hK.induction_on ?_ ?_ ?_ ?_

Premises used: IsCompact.induction_on
-- 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
refine_1 : ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ ∅ * V ⊆ U
refine_2 :
  ∀ ⦃s t : Set G⦄,
    s ⊆ t →
      (∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U) →
        ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ s * V ⊆ U
refine_3 :
  ∀ ⦃s t : Set G⦄,
    (∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ s * V ⊆ U) →
      (∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U) →
        ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ (s ∪ t) * V ⊆ U
refine_4 : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ K * V ⊆ U

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_
-- 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
⊢ Membership.mem (γ := Filter G) (𝓝 1) univ ∧ HMul.hMul (α := Set G) ∅ univ ⊆ U

Tactic:
simp
-- 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), Membership.mem (γ := Filter G) (𝓝 1) V ∧ ∅ * V ⊆ U

Tactic:
exact ⟨univ, by simp⟩
-- 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
s t : Set G
hst : s ⊆ t
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hV' : t * V ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ s * V ⊆ U

Tactic:
⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩

Premises used: HasSubset.Subset.trans, Set.mul_subset_mul_right, And.intro, Exists.intro
-- 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
s t : Set G
hst : s ⊆ t
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hV' : t * V ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ s * V ⊆ U

Tactic:
exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
-- 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
s t V : Set G
V_in : Membership.mem (γ := Filter G) (𝓝 1) V
hV' : s * V ⊆ U
W : Set G
W_in : Membership.mem (γ := Filter G) (𝓝 1) W
hW' : t * W ⊆ U
right : (s ∪ t) * (V ∩ W) ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ (s ∪ t) * V ⊆ U

Tactic:
use V ∩ W, inter_mem V_in W_in

Premises used: Filter.inter_mem
-- 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
s t V : Set G
V_in : Membership.mem (γ := Filter G) (𝓝 1) V
hV' : s * V ⊆ U
W : Set G
W_in : Membership.mem (γ := Filter G) (𝓝 1) W
hW' : t * W ⊆ U
right : s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U

Tactic:
rw [union_mul]

Premises used: Set.union_mul
-- 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
s t V : Set G
V_in : Membership.mem (γ := Filter G) (𝓝 1) V
hV' : s * V ⊆ U
W : Set G
W_in : Membership.mem (γ := Filter G) (𝓝 1) W
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U

Tactic:
union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset, Set.mul_subset_mul_left, Set.inter_subset_right
-- 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
s t V : Set G
V_in : Membership.mem (γ := Filter G) (𝓝 1) V
hV' : s * V ⊆ U
W : Set G
W_in : Membership.mem (γ := Filter G) (𝓝 1) W
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U

Tactic:
exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset, Set.mul_subset_mul_left, Set.inter_subset_right
-- 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
x : G
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 1)

Tactic:
simpa using hU.mem_nhds (hKU hx)

Premises used: IsOpen.mem_nhds
-- 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
x : G
hx : x ∈ K
⊢ Membership.mem (γ := Filter G) (map (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (x, 1))) U

Tactic:
have := tendsto_mul (show U ∈ 𝓝 (x * 1) by simpa using hU.mem_nhds (hKU hx))
-- 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
x : G
hx : x ∈ K
this : Membership.mem (γ := Filter G) (map (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (x, 1))) U
⊢ ∃ t₁ ∈ 𝓝 x, ∃ (t₂ : Set G), Membership.mem (γ := Filter G) (𝓝 1) t₂ ∧ t₁ ×ˢ t₂ ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' U

Tactic:
rw [nhds_prod_eq, mem_map, mem_prod_iff] at this

Premises used: nhds_prod_eq, Filter.mem_prod_iff, Filter.mem_map
-- 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
x : G
hx : x ∈ K
this :
  ∃ t₁ ∈ 𝓝 x, ∃ (t₂ : Set G), Membership.mem (γ := Filter G) (𝓝 1) t₂ ∧ t₁ ×ˢ t₂ ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' U
refine_4 :
  ∀ (t : Set G) (ht : t ∈ 𝓝 x) (s : Set G) (hs : Membership.mem (γ := Filter G) (𝓝 1) s)
    (h : t ×ˢ s ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' U),
    ∃ t ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U

Tactic:
rcases this with ⟨t, ht, s, hs, h⟩
-- 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
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
h : t ×ˢ s ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' U
⊢ t * s ⊆ U

Tactic:
rw [← image_subset_iff, image_mul_prod] at h

Premises used: Set.image_mul_prod, Set.image_subset_iff
-- 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
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U

Tactic:
⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

Premises used: mem_nhdsWithin_of_mem_nhds, And.intro, Exists.intro
-- 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
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U

Tactic:
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩
-- 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
rcases :
  ∀ (V : Set Gᵐᵒᵖ) (hV : Membership.mem (γ := Filter Gᵐᵒᵖ) (𝓝 (op 1)) V) (hV' : op '' K * V ⊆ op '' U),
    ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ V * K ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ V * K ⊆ U

Tactic:
rcases compact_open_separated_mul_right (hK.image continuous_op) (opHomeomorph.isOpenMap U hU)
      (image_mono hKU) with
    ⟨V, hV : V ∈ 𝓝 (op (1 : G)), hV' : op '' K * V ⊆ op '' U⟩

Premises used: MulOpposite.opHomeomorph, Set.image_mono, nhds, compact_open_separated_mul_right, OfNat.ofNat, IsCompact.image, MulOpposite.continuous_op, Homeomorph.isOpenMap, MulOpposite.op
-- 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
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ V * K ⊆ U

Tactic:
⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩

Premises used: Continuous.continuousAt, Set.preimage, And.intro, Exists.intro, MulOpposite.continuous_op, MulOpposite.op
-- 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
refine : op ⁻¹' V * K ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ V * K ⊆ U

Tactic:
refine ⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩