awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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)
    (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})
have 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)
Tactic: convert! H using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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)
⊢ 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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ 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
have 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)
Tactic: simp only [image_smul, mem_setOf_eq, mem_preimage, mem_image, Prod.exists]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
have refine_1 : ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ ∅ * V ⊆ U
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ K * V ⊆ U
have 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
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ K * V ⊆ U
have 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
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ K * V ⊆ U
have refine_4 : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ (s ∪ t) * V ⊆ U
have right : (s ∪ t) * (V ∩ W) ⊆ U
Tactic: use V ∩ W, inter_mem V_in W_in
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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 ∪ t) * (V ∩ W) ⊆ U
have right : s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
Tactic: rw [union_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
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 ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U
have this : 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))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
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 ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U
have this₁ : ∃ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U
have 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
Tactic: rcases this with ⟨t, ht, s, hs, h⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
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 ∈ 𝓝[K] x, ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ t * V ⊆ U
have h₁ : t * s ⊆ U
Tactic: rw [← image_subset_iff, image_mul_prod] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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 * K ⊆ U
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
have refine : op ⁻¹' V * K ⊆ U
Tactic: refine ⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ op ⁻¹' V * K ⊆ U
have rwa : ∀ (hV' : op '' K * op '' op ⁻¹' V ⊆ op '' 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'
Cleared hypotheses: hV'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ op ⁻¹' V * K ⊆ U
have rwa₁ : ∀ (hV' : op '' (op ⁻¹' V * K) ⊆ op '' 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'
Cleared hypotheses: hV'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ op ⁻¹' V * K ⊆ U
have rwa₂ : ∀ (hV' : op ⁻¹' V * K ⊆ op ⁻¹' op '' 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'
Cleared hypotheses: hV'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ op ⁻¹' V * K ⊆ U
have rwa₃ : ∀ (hV' : 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'
Cleared hypotheses: hV'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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)
have x : K ⊆ ⋃ (i : G), (fun (x : G) ↦ (interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V) : Set G)) i
Tactic: refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ K ⊆ ⋃ (i : G), (fun (x : G) ↦ (interior ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V) : Set G)) i
have 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
Tactic: obtain ⟨g₀, hg₀⟩ := hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
have refine : ∀ g ∈ K, Membership.mem (γ := Set G) (interior ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' V)) g
Tactic: refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ Membership.mem (γ := Set G) (interior ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' V)) g
have refine : Membership.mem (γ := Set G) ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' interior V) g
Tactic: refine preimage_interior_subset_interior_preimage (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ Membership.mem (γ := Set G) ((fun (x : G) ↦ g₀ * g⁻¹ * x) ⁻¹' interior V) g
have rwa : g₀ * g⁻¹ * g ∈ interior V
Tactic: rwa [mem_preimage, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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 ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ SigmaCompactSpace G
have obtain : ∀ (L : Set G) (hLc : IsCompact L) (hL1 : Membership.mem (γ := Filter G) (𝓝 1) L), SigmaCompactSpace G
Tactic: obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
have refine_1 : ∀ (n : ℕ), IsCompact.{w} (X := G) ((fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n)
Tactic: refine ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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)
⊢ SigmaCompactSpace G
have refine_2 : Eq.{w + 1} (α := Set G) (⋃ (n : ℕ), (fun (n : ℕ) ↦ ((fun (x : G) ↦ x * denseSeq G n) ⁻¹' L : Set G)) n) univ
Tactic: refine ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
have refine_2 : ∀ (x : G), ∃ (i : ℕ), Membership.mem (γ := Set G) ((fun (x : G) ↦ x * denseSeq G i) ⁻¹' L) x
Tactic: refine iUnion_eq_univ_iff.2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
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
⊢ (range (denseSeq G) ∩ (fun (y : G) ↦ x * y) ⁻¹' L).Nonempty
have hL1₁ : 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
Cleared hypotheses: hL1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ ∃ (i : ℕ), Membership.mem (γ := Set G) ((fun (x : G) ↦ x * denseSeq G i) ⁻¹' L) x
have 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
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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
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
⊢ ∃ (g : G), Disjoint K (g • L)
have A : ¬K * L⁻¹ = univ
Tactic: have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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), g ∉ K * L⁻¹
have contrapose! : ∀ (A : ∀ (g : G), g ∈ K * L⁻¹), K * L⁻¹ = univ
Tactic: contrapose! A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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), Disjoint K (g • L)
have obtain : ∀ (g : G) (hg : g ∉ K * 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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)
have refine : Disjoint K (g • L)
Tactic: refine ⟨g, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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)
have refine : ∀ (a : G) (ha : a ∈ K) (h'a : a ∈ g • L), g ∈ K * L⁻¹
Tactic: refine disjoint_left.2 fun a ha h'a => hg ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ g ∈ K * L⁻¹
have rcases : ∀ (b : G) (bL : b ∈ L) (ha : (fun (x : G) ↦ g • x) b ∈ K), g ∈ K * L⁻¹
Tactic: rcases h'a with ⟨b, bL, rfl⟩
Cleared hypotheses: a, ha, h'a
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ g ∈ K * L⁻¹
have refine : (fun (x1 x2 : G) ↦ x1 * x2) (g * b) b⁻¹ = g
Tactic: refine ⟨g * b, ha, b⁻¹, by simpa only [Set.mem_inv, inv_inv] using bL, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
⊢ 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))
have 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))
Tactic: rw [← map₂_mul, map_map₂, map_map₂]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← map₂_mul, map_map₂, map_map₂]