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₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
hm :
  ∀ (i : G) (j : i ∈ s),
    Subset (α := Set G) ((fun (h : G) ↦ i * h) ⁻¹' (↑K₀ : Set G)) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)
⊢ Subset.{u_1} (α := Set G) (⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G))
    (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)

Tactic:
apply iUnion₂_subset

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
g₁ : G
hg₁ : g₁ ∈ s
hm : ∀ (a : G), g₁ * a ∈ (↑K₀ : Set G) → Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) a
⊢ Subset (α := Set G) ((fun (h : G) ↦ g₁ * h) ⁻¹' (↑K₀ : Set G)) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)

Tactic:
rw [preimage_subset_iff]

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

Tactic:
have := h1t hg₂
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)
this : Membership.mem (γ := Set G) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (g₁ * g₂)
hm :
  ∀ (g₃ : G) (hg₃ : g₃ ∈ t)
    (h2V : Membership.mem (γ := Set G) ((fun (h : g₃ ∈ t) ↦ ((fun (h : G) ↦ g₃ * h) ⁻¹' V : Set G)) hg₃) (g₁ * g₂)),
    Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
⊢ Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂

Tactic:
rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩

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₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)
g₃ : G
hg₃ : g₃ ∈ t
h2V : Membership.mem (γ := Set G) ((fun (h : g₃ ∈ t) ↦ ((fun (h : G) ↦ g₃ * h) ⁻¹' V : Set G)) hg₃) (g₁ * g₂)
⊢ g₃ * g₁ * g₂ ∈ V

Tactic:
rw [mem_preimage, ← mul_assoc] at h2V

Premises used: mul_assoc, 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₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₃ * g₁ * g₂ ∈ V
⊢ Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂

Tactic:
mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V

Premises used: Set.Mem, Set.mem_biUnion, Finset.mul_mem_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₃ * g₁ * g₂ ∈ V
⊢ Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂

Tactic:
exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V

Premises used: Set.mem_biUnion, Finset.mul_mem_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
rw :
  ¬∃ (x : Finset G),
      Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} x ∧
        x.card = 0
rw₁ :
  (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
⊢ 0 < index (↑K : Set G) V

Tactic:
rw [index, Nat.sInf_def, Nat.find_pos, mem_image]

Premises used: Set.mem_image, Nat.sInf_def, MeasureTheory.Measure.haar.index, Nat.find_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
t : Finset G
h1t : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} t
h2t : t.card = 0
⊢ t = ∅

Tactic:
rw [Finset.card_eq_zero] at h2t

Premises used: Finset.card_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
t : Finset G
h1t : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} t
h2t : t = ∅
⊢ Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} ∅

Tactic:
subst h2t
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} ∅
obtain : ∀ (g : G) (hg : g ∈ interior (↑K : Set G)), False
⊢ False

Tactic:
obtain ⟨g, hg⟩ := K.interior_nonempty

Premises used: TopologicalSpace.PositiveCompacts.interior_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} ∅
g : G
hg : g ∈ interior (↑K : Set G)
⊢ Membership.mem (γ := Set G) (⋃ (g : G), ⋃ (_ : Membership.mem (γ := Finset G) ∅ g), (fun (h : G) ↦ g * h) ⁻¹' V) g

Tactic:
h1t (interior_subset hg)

Premises used: interior_subset
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} ∅
g : G
hg : g ∈ interior (↑K : Set G)
h : Eq.{u_1 + 1} (α := Set G) ∅ (⋃ (g : G), ⋃ (_ : Membership.mem (γ := Finset G) ∅ g), (fun (h : G) ↦ g * h) ⁻¹' V)
⊢ Membership.mem (γ := Set G) ∅ g

Tactic:
convert! h1t (interior_subset hg)

Premises used: interior_subset
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} ∅
g : G
hg : g ∈ interior (↑K : Set G)
h : Eq.{u_1 + 1} (α := Set G) (⋃ (g : G), ⋃ (_ : Membership.mem (γ := Finset G) ∅ g), (fun (h : G) ↦ g * h) ⁻¹' V) ∅
⊢ Eq.{u_1 + 1} (α := Set G) ∅ (⋃ (g : G), ⋃ (_ : Membership.mem (γ := Finset G) ∅ g), (fun (h : G) ↦ g * h) ⁻¹' V)

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} ∅
g : G
hg : g ∈ interior (↑K : Set G)
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ (g : G), ⋃ (_ : Membership.mem (γ := Finset G) ∅ g), (fun (h : G) ↦ g * h) ⁻¹' V) ∅

Tactic:
simp only [Finset.notMem_empty, iUnion_of_empty, iUnion_empty]

Premises used: Finset.notMem_empty, Set.iUnion_of_empty, Set.iUnion_empty
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty

Tactic:
index_defined K.isCompact hV

Premises used: Set.Nonempty, MeasureTheory.Measure.haar.index_defined, TopologicalSpace.PositiveCompacts.isCompact
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty

Tactic:
exact index_defined K.isCompact hV

Premises used: MeasureTheory.Measure.haar.index_defined, TopologicalSpace.PositiveCompacts.isCompact
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
rw :
  0 <
    sInf
      (image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V})
rw₁ :
  0 <
    Nat.find (p := fun (n : ℕ) ↦
      n ∈
        image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V})
      ⋯
rw₂ :
  (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
rw₃ :
  0 ∉ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
rw₄ :
  (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
rw₅ :
  ¬∃ (x : Finset G),
      Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} x ∧
        x.card = 0
rw₆ :
  (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
rw₇ :
  ¬∃ (x : Finset G),
      Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} x ∧
        x.card = 0
rw₈ :
  (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
rw₉ :
  ¬∃ (x : Finset G),
      Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} x ∧
        x.card = 0
rw₁₀ rw₁₁ :
  (image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
⊢ 0 < index (↑K : Set G) V

Tactic:
classical
  rw [index, Nat.sInf_def, Nat.find_pos, mem_image]
  · rintro ⟨t, h1t, h2t⟩; rw [Finset.card_eq_zero] at h2t; subst h2t
    obtain ⟨g, hg⟩ := K.interior_nonempty
    change g ∈ (∅ : Set G)
    convert! h1t (interior_subset hg); symm
    simp only [Finset.notMem_empty, iUnion_of_empty, iUnion_empty]
  · exact index_defined K.isCompact hV

Premises used: TopologicalSpace.PositiveCompacts.interior_nonempty, Set.mem_image, Nat.sInf_def, MeasureTheory.Measure.haar.index, Finset.notMem_empty, Set.iUnion_of_empty, Nat.find_pos, Finset.card_eq_zero, MeasureTheory.Measure.haar.index_defined, Set.iUnion_empty, EmptyCollection.emptyCollection, TopologicalSpace.PositiveCompacts.isCompact
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
rcases :
  ∀ (s : Finset G) (h1s : K' ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K' V), index K V ≤ index K' V
⊢ index K V ≤ index K' V

Tactic:
rcases index_elim hK' hV with ⟨s, h1s, h2s⟩

Premises used: MeasureTheory.Measure.haar.index_elim
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K' V
hm : index K' V ∈ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
⊢ index K V ≤ index K' V

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' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ ∃ (x : Finset G),
    Membership.mem (γ := Set (Finset G)) {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} x ∧
      x.card = index K' V

Tactic:
⟨s, Subset.trans h h1s, h2s⟩

Premises used: Set.Subset.trans, 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' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ ∃ (x : Finset G),
    Membership.mem (γ := Set (Finset G)) {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} x ∧
      x.card = index K' V

Tactic:
exact ⟨s, Subset.trans h h1s, h2s⟩
-- 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
rcases :
  ∀ (s : Finset G) (h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K₁.carrier V),
    index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V

Tactic:
rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩

Premises used: MeasureTheory.Measure.haar.index_elim, TopologicalSpace.Compacts.isCompact'
-- 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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
rcases :
  ∀ (t : Finset G) (h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (h2t : t.card = index K₂.carrier V),
    index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V

Tactic:
rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩

Premises used: MeasureTheory.Measure.haar.index_elim, TopologicalSpace.Compacts.isCompact'
-- 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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
rw : index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V

Tactic:
rw [← h2s, ← h2t]
-- 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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card

Tactic:
le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_le _ _)

Premises used: Finset.card_union_le, Nat.sInf_le, And.intro, Exists.intro, rfl, 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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
refine :
  Membership.mem (γ := Set (Finset G)) {t : Finset G | K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
    (s ∪ t)
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card

Tactic:
refine le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
rw : K₁.carrier ∪ K₂.carrier ⊆ (⋃ x ∈ s, (fun (h : G) ↦ x * h) ⁻¹' V) ∪ ⋃ x ∈ t, (fun (h : G) ↦ x * h) ⁻¹' V
⊢ Membership.mem (γ := Set (Finset G)) {t : Finset G | K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
    (s ∪ t)

Tactic:
rw [mem_setOf_eq, Finset.set_biUnion_union]

Premises used: Set.mem_setOf_eq, Finset.set_biUnion_union
-- 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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ K₁.carrier ∪ K₂.carrier ⊆ (⋃ x ∈ s, (fun (h : G) ↦ x * h) ⁻¹' V) ∪ ⋃ x ∈ t, (fun (h : G) ↦ x * h) ⁻¹' V

Tactic:
gcongr
-- 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
rcases :
  ∀ (s : Finset G) (h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K₁.carrier V),
    index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
rcases₁ :
  ∀ (s : Finset G) (h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K₁.carrier V)
    (t : Finset G) (h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (h2t : t.card = index K₂.carrier V),
    index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
rcases₂ :
  ∀ (s : Finset G) (h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K₁.carrier V)
    (t : Finset G) (h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (h2t : t.card = index K₂.carrier V),
    index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card
rcases₃ :
  ∀ (s : Finset G) (h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K₁.carrier V)
    (t : Finset G) (h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (h2t : t.card = index K₂.carrier V),
    Membership.mem (γ := Set (Finset G)) {t : Finset G | K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
      (s ∪ t)
rcases₄ :
  ∀ (s : Finset G) (h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K₁.carrier V)
    (t : Finset G) (h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (h2t : t.card = index K₂.carrier V),
    K₁.carrier ∪ K₂.carrier ⊆ (⋃ x ∈ s, (fun (h : G) ↦ x * h) ⁻¹' V) ∪ ⋃ x ∈ t, (fun (h : G) ↦ x * h) ⁻¹' V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V

Tactic:
classical
  rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩
  rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩
  rw [← h2s, ← h2t]
  refine le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_le _ _)
  rw [mem_setOf_eq, Finset.set_biUnion_union]
  gcongr

Premises used: MeasureTheory.Measure.haar.index_elim, TopologicalSpace.Compacts.isCompact', Set.mem_setOf_eq, Finset.set_biUnion_union
-- 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⁻¹)
apply : index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
⊢ index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V

Tactic:
apply le_antisymm (index_union_le K₁ K₂ hV)

Premises used: le_antisymm, MeasureTheory.Measure.haar.index_union_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⁻¹)
rcases :
  ∀ (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),
    index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V

Tactic:
rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩

Premises used: MeasureTheory.Measure.haar.index_elim, TopologicalSpace.Compacts.isCompact', IsCompact.union
-- 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
rw : index K₁.carrier V + index K₂.carrier V ≤ s.card
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V

Tactic:
rw [← h2s]