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₁ 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
have refine : Membership.mem (γ := Set (Finset G)) {t : Finset G | K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
  (s ∪ t)
Tactic: refine le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_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
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)
have rw : K₁.carrier ∪ K₂.carrier ⊆ (⋃ x ∈ s, (fun (h : G) ↦ x * h) ⁻¹' V) ∪ ⋃ x ∈ t, (fun (h : G) ↦ x * h) ⁻¹' V
Tactic: rw [mem_setOf_eq, Finset.set_biUnion_union]
-- 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: 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
-- 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
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
have 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
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
-- 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
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
⊢ 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)
  (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: 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
-- 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
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
⊢ 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)
  (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)
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
-- 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
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)
⊢ 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)
  (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: 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
-- 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: apply le_antisymm (index_union_le K₁ K₂ 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₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
have 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
Tactic: rcases index_elim (K₁.2.union 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
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
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
have rw : index K₁.carrier V + index K₂.carrier 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₁ 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
have 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}
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
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}
have 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})
Tactic: refine ⟨_, ?_, rfl⟩
-- 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
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
⊢ Membership.mem (γ := Set G) (⋃ g ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun (h : G) ↦ g * h) ⁻¹' V)
    g
have 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
Tactic: rcases hK hg with ⟨_, ⟨g₀, rfl⟩, _, ⟨h1g₀, rfl⟩, h2g₀⟩
-- 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
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
⊢ Membership.mem (γ := Set G) (⋃ g ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun (h : G) ↦ g * h) ⁻¹' V)
    g
have h2g₁ : g₀ * g ∈ V
Tactic: simp only [mem_preimage] at h2g₀
Cleared hypotheses: h2g₀
-- 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
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) (⋃ g ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun (h : G) ↦ g * h) ⁻¹' V)
    g
have 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
Tactic: simp only [mem_iUnion]
-- 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
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
⊢ ∃ (i : G) (_ : i ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
    Membership.mem (γ := Set G) ((fun (h : G) ↦ i * h) ⁻¹' V) g
have h₁ : ∃ (_ : g₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
  Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g
Tactic: use 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
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₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
    Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g
have h₁ : Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g
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
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
⊢ ∃ (_ : g₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}),
    Membership.mem (γ := Set G) ((fun (h : G) ↦ g₀ * h) ⁻¹' V) g
have h₂ : g₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}
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
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₀ ∈ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}
have h₁ : ((fun (x : G) ↦ g₀ * x) ⁻¹' V ∩ K).Nonempty
Tactic: simp only [Finset.mem_filter, h1g₀, true_and]
-- 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
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
⊢ ((fun (x : G) ↦ g₀ * x) ⁻¹' V ∩ K).Nonempty
have h₁ : g ∈ (fun (x : G) ↦ g₀ * x) ⁻¹' V ∩ K
Tactic: use g
-- 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
⊢ index K₁.carrier V + index K₂.carrier V ≤ s.card
have 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
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₀
-- 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
⊢ index K₁.carrier V + index K₂.carrier V ≤ s.card
have 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
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)) ?_
-- 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 ∈ 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
have 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
Tactic: rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
-- 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
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
⊢ {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
have rw₁ : Disjoint ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty})
  ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty})
Tactic: rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
-- 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
⊢ Disjoint ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty})
    ({g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty})
have 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
Tactic: apply Finset.disjoint_filter.mpr
-- 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
⊢ False
have h1g₄ : g₁ * g₃ ∈ V
Tactic: simp only [mem_preimage] at h1g₃ h1g₂
Cleared hypotheses: h1g₂, h1g₃