awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have obtain : ∀ (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)),
  index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
Tactic: classical
  obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
  rw [← h2s, ← h2t, mul_comm]
  refine le_trans ?_ Finset.card_mul_le
  apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]; refine Subset.trans h1s ?_
  apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
  have := h1t hg₂
  rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
  exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
obtain :
  ∀ (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)),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have obtain₁ : ∀ (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),
  index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
Tactic: classical
  obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
  rw [← h2s, ← h2t, mul_comm]
  refine le_trans ?_ Finset.card_mul_le
  apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]; refine Subset.trans h1s ?_
  apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
  have := h1t hg₂
  rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
  exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
obtain :
  ∀ (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)),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
obtain₁ :
  ∀ (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),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have obtain₂ : ∀ (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),
  index (↑K : Set G) V ≤ t.card * s.card
Tactic: classical
  obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
  rw [← h2s, ← h2t, mul_comm]
  refine le_trans ?_ Finset.card_mul_le
  apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]; refine Subset.trans h1s ?_
  apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
  have := h1t hg₂
  rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
  exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
obtain :
  ∀ (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)),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
obtain₁ :
  ∀ (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),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
obtain₂ :
  ∀ (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),
    index (↑K : Set G) V ≤ t.card * s.card
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have obtain₃ : ∀ (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),
  index (↑K : Set G) V ≤ (t * s).card
Tactic: classical
  obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
  rw [← h2s, ← h2t, mul_comm]
  refine le_trans ?_ Finset.card_mul_le
  apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]; refine Subset.trans h1s ?_
  apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
  have := h1t hg₂
  rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
  exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
obtain :
  ∀ (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)),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
obtain₁ :
  ∀ (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),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
obtain₂ :
  ∀ (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),
    index (↑K : Set G) V ≤ t.card * s.card
obtain₃ :
  ∀ (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),
    index (↑K : Set G) V ≤ (t * s).card
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have hm : ∀ (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),
  (t * s).card ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
Tactic: classical
  obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
  rw [← h2s, ← h2t, mul_comm]
  refine le_trans ?_ Finset.card_mul_le
  apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]; refine Subset.trans h1s ?_
  apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
  have := h1t hg₂
  rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
  exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
obtain :
  ∀ (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)),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
obtain₁ :
  ∀ (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),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
obtain₂ :
  ∀ (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),
    index (↑K : Set G) V ≤ t.card * s.card
obtain₃ :
  ∀ (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),
    index (↑K : Set G) V ≤ (t * s).card
hm hm₁ :
  ∀ (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),
    (t * s).card ∈
      image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have hm₂ : ∀ (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),
  Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} (t * s)
Tactic: classical
  obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
  rw [← h2s, ← h2t, mul_comm]
  refine le_trans ?_ Finset.card_mul_le
  apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_setOf_eq]; refine Subset.trans h1s ?_
  apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
  have := h1t hg₂
  rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
  exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ 0 < index (↑K : Set G) V
have 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
Tactic: rw [index, Nat.sInf_def, Nat.find_pos, mem_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ 0 < index (↑K : Set G) V
have rw₁ : (image.{u_1, 0} (α := Finset G) Finset.card
    {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
Tactic: rw [index, Nat.sInf_def, Nat.find_pos, mem_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
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
⊢ False
have h2t₁ : t = ∅
Tactic: rw [Finset.card_eq_zero] at h2t
Cleared hypotheses: h2t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
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 = ∅
⊢ False
have h1t₁ : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} ∅
Tactic: subst h2t
Cleared hypotheses: t, h1t, h2t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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} ∅
⊢ False
have obtain : ∀ (g : G) (hg : g ∈ interior (↑K : Set G)), False
Tactic: obtain ⟨g, hg⟩ := K.interior_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
have h : Eq.{u_1 + 1} (α := Set G) ∅ (⋃ (g : G), ⋃ (_ : Membership.mem (γ := Finset G) ∅ g), (fun (h : G) ↦ g * h) ⁻¹' V)
Tactic: convert! h1t (interior_subset hg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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)
have h : Eq.{u_1 + 1} (α := Set G) (⋃ (g : G), ⋃ (_ : Membership.mem (γ := Finset G) ∅ g), (fun (h : G) ↦ g * h) ⁻¹' V) ∅
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ 0 < index (↑K : Set G) V
have 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})
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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})
⊢ 0 < index (↑K : Set G) V
have 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})
    sorry
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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})
      ⋯
⊢ 0 < index (↑K : Set G) V
have rw₂ : (image.{u_1, 0} (α := Finset G) Finset.card
    {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}).Nonempty
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ 0 < index (↑K : Set G) V
have rw₃ : 0 ∉ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ 0 < index (↑K : Set G) V
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ index K V ≤ index K' V
have 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
Tactic: rcases index_elim hK' hV with ⟨s, h1s, h2s⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ index K V ≤ index K' V
have hm : index K' V ∈ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
Tactic: apply Nat.sInf_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
have 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
Tactic: rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
have 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
Tactic: rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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 ≤ index K₁.carrier V + index K₂.carrier V
have rw : index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card
Tactic: rw [← h2s, ← h2t]