awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
hm :
  {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
⊢ index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card

Tactic:
apply Nat.sInf_le

Premises used: Nat.sInf_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
⊢ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
⟨_, ?_, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
hm :
  Membership.mem (γ := Set (Finset G)) {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
    ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty})
⊢ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
refine ⟨_, ?_, rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
hm :
  ∀ (g₀ : G) (h1g₀ : g₀ ∈ s)
    (h2g₀ : Membership.mem (γ := Set G) ((fun (h : g₀ ∈ s) ↦ ((fun (x : G) ↦ g₀ * x) ⁻¹' V : Set G)) h1g₀) g),
    Membership.mem (γ := Set G)
      (⋃ g ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun (h : G) ↦ g * h) ⁻¹' V) g
⊢ Membership.mem (γ := Set G) (⋃ g ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun (h : G) ↦ g * h) ⁻¹' V)
    g

Tactic:
rcases hK hg with ⟨_, ⟨g₀, rfl⟩, _, ⟨h1g₀, rfl⟩, h2g₀⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : Membership.mem (γ := Set G) ((fun (h : g₀ ∈ s) ↦ ((fun (x : G) ↦ g₀ * x) ⁻¹' V : Set G)) h1g₀) g
⊢ g₀ * g ∈ V

Tactic:
simp only [mem_preimage] at h2g₀

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
hm :
  ∃ (i : G) (_ : i ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
    Membership.mem (γ := Set G) ((fun (h : G) ↦ i * h) ⁻¹' V) g
⊢ Membership.mem (γ := Set G) (⋃ g ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun (h : G) ↦ g * h) ⁻¹' V)
    g

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
h₁ :
  ∃ (_ : g₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
    Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g
⊢ ∃ (i : G) (_ : i ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
    Membership.mem (γ := Set G) ((fun (h : G) ↦ i * h) ⁻¹' V) g

Tactic:
use g₀
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
h₁ : Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g
h₂ : g₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}
⊢ ∃ (_ : g₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
    Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
h₁ : ((fun (x : G) ↦ g₀ * x) ⁻¹' V ∩ K).Nonempty
⊢ g₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}

Tactic:
simp only [Finset.mem_filter, h1g₀, true_and]

Premises used: Finset.mem_filter, true_and
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
h₁ : g ∈ (fun (x : G) ↦ g₀ * x) ⁻¹' V ∩ K
⊢ ((fun (x : G) ↦ g₀ * x) ⁻¹' V ∩ K).Nonempty

Tactic:
use g
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun (x : G) ↦ g₀ * x) ⁻¹' V ∩ K

Tactic:
simp [hg, h2g₀]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g

Tactic:
h2g₀

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g

Tactic:
exact h2g₀
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
⊢ ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card

Tactic:
have (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (g * ·) ⁻¹' V) :
      index K V ≤ {g ∈ s | ((g * ·) ⁻¹' V ∩ K).Nonempty}.card := by
    apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]
    intro g hg; rcases hK hg with ⟨_, ⟨g₀, rfl⟩, _, ⟨h1g₀, rfl⟩, h2g₀⟩
    simp only [mem_preimage] at h2g₀
    simp only [mem_iUnion]; use g₀; constructor; swap
    · simp only [Finset.mem_filter, h1g₀, true_and]; use g
      simp [hg, h2g₀]
    exact h2g₀
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ index K₁.carrier V + index K₂.carrier V ≤ s.card

Tactic:
le_trans
      (add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s)
        (this K₂.1 <| Subset.trans subset_union_right h1s)) ?_

Premises used: Set.Subset.trans, add_le_add, Set.subset_union_right, TopologicalSpace.Compacts.carrier, Set.subset_union_left, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
subset_union_left :
  {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty}.card +
      {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card
⊢ index K₁.carrier V + index K₂.carrier V ≤ s.card

Tactic:
refine
    le_trans
      (add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s)
        (this K₂.1 <| Subset.trans subset_union_right h1s)) ?_

Premises used: Set.Subset.trans, add_le_add, Set.subset_union_right, TopologicalSpace.Compacts.carrier, Set.subset_union_left, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
rw :
  {x ∈ s |
        ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty ∨
          ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card
rw₁ :
  Disjoint ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty})
    ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty})
⊢ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty}.card +
      {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card

Tactic:
rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]

Premises used: Finset.filter_union_right, Finset.card_union_of_disjoint
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ {x ∈ s |
        ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty ∨
          ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card

Tactic:
s.card_filter_le _

Premises used: Finset.card_filter_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ {x ∈ s |
        ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty ∨
          ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card

Tactic:
exact s.card_filter_le _

Premises used: Finset.card_filter_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
apply :
  ∀ x ∈ s,
    ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty → ¬((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty
⊢ Disjoint ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty})
    ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty})

Tactic:
apply Finset.disjoint_filter.mpr

Premises used: Iff.mpr, Finset.disjoint_filter
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h1g₂ : Membership.mem (γ := Set G) ((fun (x : G) ↦ g₁ * x) ⁻¹' V) g₂
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h1g₃ : Membership.mem (γ := Set G) ((fun (x : G) ↦ g₁ * x) ⁻¹' V) g₃
h2g₃ : g₃ ∈ K₂.carrier
⊢ g₁ * g₃ ∈ V

Tactic:
simp only [mem_preimage] at h1g₃ h1g₂

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h1g₂ : Membership.mem (γ := Set G) ((fun (x : G) ↦ g₁ * x) ⁻¹' V) g₂
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h1g₃ : Membership.mem (γ := Set G) ((fun (x : G) ↦ g₁ * x) ⁻¹' V) g₃
h2g₃ : g₃ ∈ K₂.carrier
h1g₄ : g₁ * g₃ ∈ V
⊢ g₁ * g₂ ∈ V

Tactic:
simp only [mem_preimage] at h1g₃ h1g₂

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ False

Tactic:
h.le_bot (?_ : g₁⁻¹ ∈ _)

Premises used: Disjoint.le_bot, Set.Mem
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
refine : g₁⁻¹ ∈ K₁.carrier * V⁻¹ ⊓ K₂.carrier * V⁻¹
⊢ False

Tactic:
refine h.le_bot (?_ : g₁⁻¹ ∈ _)

Premises used: Disjoint.le_bot
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
left : g₁⁻¹ ∈ K₁.carrier * V⁻¹
right : g₁⁻¹ ∈ K₂.carrier * V⁻¹
⊢ g₁⁻¹ ∈ K₁.carrier * V⁻¹ ⊓ K₂.carrier * V⁻¹

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
left : ∃ x ∈ K₁.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹
⊢ g₁⁻¹ ∈ K₁.carrier * V⁻¹

Tactic:
simp only [Set.mem_inv, Set.mem_mul]

Premises used: Set.mem_mul, Set.mem_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
right : ∃ x ∈ K₂.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹
⊢ g₁⁻¹ ∈ K₂.carrier * V⁻¹

Tactic:
simp only [Set.mem_inv, Set.mem_mul]

Premises used: Set.mem_mul, Set.mem_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x ∈ K₁.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹

Tactic:
⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩

Premises used: HMul.hMul, Inv.inv, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
left : (g₁ * g₂)⁻¹⁻¹ ∈ V
left₁ : g₂ * (g₁ * g₂)⁻¹ = g₁⁻¹
⊢ ∃ x ∈ K₁.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹

Tactic:
refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₂)⁻¹⁻¹ ∈ V

Tactic:
simp only [inv_inv, h1g₂]

Premises used: inv_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₂ * (g₁ * g₂)⁻¹ = g₁⁻¹

Tactic:
simp only [mul_inv_rev, mul_inv_cancel_left]

Premises used: mul_inv_rev, mul_inv_cancel_left