awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ 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
⊢ False
have h1g₅ : g₁ * g₂ ∈ V
Tactic: simp only [mem_preimage] at h1g₃ h1g₂
Cleared hypotheses: h1g₂, h1g₃
-- 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
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
have refine : g₁⁻¹ ∈ K₁.carrier * V⁻¹ ⊓ K₂.carrier * V⁻¹
Tactic: refine h.le_bot (?_ : g₁⁻¹ ∈ _)
-- 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
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₁⁻¹ ∈ K₁.carrier * V⁻¹ ⊓ K₂.carrier * V⁻¹
have left : g₁⁻¹ ∈ K₁.carrier * V⁻¹
Tactic: constructor
-- 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
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⁻¹
⊢ g₁⁻¹ ∈ K₁.carrier * V⁻¹ ⊓ K₂.carrier * V⁻¹
have right : g₁⁻¹ ∈ K₂.carrier * V⁻¹
Tactic: constructor
-- 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
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₁⁻¹ ∈ K₁.carrier * V⁻¹
have left : ∃ x ∈ K₁.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹
Tactic: simp only [Set.mem_inv, Set.mem_mul]
-- 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
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₁⁻¹ ∈ K₂.carrier * V⁻¹
have right : ∃ x ∈ K₂.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹
Tactic: simp only [Set.mem_inv, Set.mem_mul]
-- 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
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₁⁻¹
have left : (g₁ * g₂)⁻¹⁻¹ ∈ V
Tactic: refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
-- 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
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
⊢ ∃ x ∈ K₁.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹
have left₁ : g₂ * (g₁ * g₂)⁻¹ = g₁⁻¹
Tactic: refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
-- 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
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₁⁻¹
have right : (g₁ * g₃)⁻¹⁻¹ ∈ V
Tactic: refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
-- 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
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 : (g₁ * g₃)⁻¹⁻¹ ∈ V
⊢ ∃ x ∈ K₂.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹
have right₁ : g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹
Tactic: refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
-- 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
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
⊢ index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V
have apply : index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
Tactic: classical
  apply le_antisymm (index_union_le K₁ K₂ hV)
  rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩; rw [← h2s]
  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₀
  refine
    le_trans
      (add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s)
        (this K₂.1 <| Subset.trans subset_union_right h1s)) ?_
  rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
  · exact s.card_filter_le _
  apply Finset.disjoint_filter.mpr
  rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
  simp only [mem_preimage] at h1g₃ h1g₂
  refine h.le_bot (?_ : g₁⁻¹ ∈ _)
  constructor <;> simp only [Set.mem_inv, Set.mem_mul]
  · refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₂]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
  · refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₃]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
-- 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
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
have apply₁ : ∀ (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
Tactic: classical
  apply le_antisymm (index_union_le K₁ K₂ hV)
  rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩; rw [← h2s]
  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₀
  refine
    le_trans
      (add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s)
        (this K₂.1 <| Subset.trans subset_union_right h1s)) ?_
  rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
  · exact s.card_filter_le _
  apply Finset.disjoint_filter.mpr
  rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
  simp only [mem_preimage] at h1g₃ h1g₂
  refine h.le_bot (?_ : g₁⁻¹ ∈ _)
  constructor <;> simp only [Set.mem_inv, Set.mem_mul]
  · refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₂]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
  · refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₃]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
-- 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
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
apply : index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
apply₁ apply₂ :
  ∀ (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 ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V
have apply₃ : ∀ (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 ≤ s.card
Tactic: classical
  apply le_antisymm (index_union_le K₁ K₂ hV)
  rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩; rw [← h2s]
  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₀
  refine
    le_trans
      (add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s)
        (this K₂.1 <| Subset.trans subset_union_right h1s)) ?_
  rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
  · exact s.card_filter_le _
  apply Finset.disjoint_filter.mpr
  rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
  simp only [mem_preimage] at h1g₃ h1g₂
  refine h.le_bot (?_ : g₁⁻¹ ∈ _)
  constructor <;> simp only [Set.mem_inv, Set.mem_mul]
  · refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₂]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
  · refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₃]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
-- 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
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
apply : index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
apply₁ apply₂ :
  ∀ (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
apply₃ :
  ∀ (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 ≤ s.card
⊢ index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V
have apply₄ : ∀ (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: classical
  apply le_antisymm (index_union_le K₁ K₂ hV)
  rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩; rw [← h2s]
  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₀
  refine
    le_trans
      (add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s)
        (this K₂.1 <| Subset.trans subset_union_right h1s)) ?_
  rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
  · exact s.card_filter_le _
  apply Finset.disjoint_filter.mpr
  rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
  simp only [mem_preimage] at h1g₃ h1g₂
  refine h.le_bot (?_ : g₁⁻¹ ∈ _)
  constructor <;> simp only [Set.mem_inv, Set.mem_mul]
  · refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₂]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
  · refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₃]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
-- 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
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
apply : index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
apply₁ apply₂ :
  ∀ (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
apply₃ :
  ∀ (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 ≤ s.card
apply₄ :
  ∀ (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
⊢ index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V
have apply₅ : ∀ (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 ∈ 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: classical
  apply le_antisymm (index_union_le K₁ K₂ hV)
  rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩; rw [← h2s]
  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₀
  refine
    le_trans
      (add_le_add (this K₁.1 <| Subset.trans subset_union_left h1s)
        (this K₂.1 <| Subset.trans subset_union_right h1s)) ?_
  rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
  · exact s.card_filter_le _
  apply Finset.disjoint_filter.mpr
  rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
  simp only [mem_preimage] at h1g₃ h1g₂
  refine h.le_bot (?_ : g₁⁻¹ ∈ _)
  constructor <;> simp only [Set.mem_inv, Set.mem_mul]
  · refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₂]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
  · refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₃]
    · simp only [mul_inv_rev, mul_inv_cancel_left]
-- 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
⊢ index ((fun (h : G) ↦ g * h) '' 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 ((fun (h : G) ↦ g * h) '' 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ index ((fun (h : G) ↦ g * h) '' K) V ≤ index K V
have rw : index ((fun (h : G) ↦ g * h) '' K) V ≤ s.card
Tactic: rw [← 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ index ((fun (h : G) ↦ g * h) '' K) V ≤ s.card
have hm : s.card ∈
  image.{u_1, 0} (α := Finset G) Finset.card
    {t : Finset G | Subset (α := Set G) ((fun (h : G) ↦ g * h) '' 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
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 | Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V)} x ∧
      x.card = s.card
have hm : Membership.mem (γ := Set (Finset G))
  {t : Finset G | Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V)}
  (Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s)
Tactic: refine ⟨s.map (Equiv.mulRight g⁻¹).toEmbedding, ?_, Finset.card_map _⟩
-- 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K)
    (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)
have hm : Subset.{u_1} (α := Set G) ((fun (h : G) ↦ g * h) '' ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V)
  (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)
Tactic: refine Subset.trans (image_mono h1s) ?_
-- 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : Membership.mem (γ := Set G) ((fun (h : g₂ ∈ s) ↦ ((fun (h : G) ↦ g₂ * h) ⁻¹' V : Set G)) hg₂) g₁
⊢ Membership.mem (γ := Set G)
    (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)
    ((fun (h : G) ↦ g * h) g₁)
have hg₃ : g₂ * g₁ ∈ V
Tactic: simp only [mem_preimage] at hg₁
Cleared hypotheses: 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ Membership.mem (γ := Set G)
    (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)
    ((fun (h : G) ↦ g * h) g₁)
have hm : ∃ a ∈ s, a * g⁻¹ * (g * g₁) ∈ V
Tactic: simp only [exists_prop, mem_iUnion, Finset.mem_map, Equiv.coe_mulRight,
    exists_exists_and_eq_and, mem_preimage, Equiv.toEmbedding_apply]
-- 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ ∃ a ∈ s, a * g⁻¹ * (g * g₁) ∈ V
have hm : g₂ * g⁻¹ * (g * g₁) ∈ V
Tactic: refine ⟨_, hg₂, ?_⟩