-- 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
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}
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),
    Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} (t * s)
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),
    (↑K : Set G) ⊆ ⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V
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),
    Subset.{u_1} (α := Set G) (⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G))
      (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)
hm₇ hm₈ 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) (g₁ : G)
    (hg₁ : g₁ ∈ s),
    Subset (α := Set G) ((fun (h : G) ↦ g₁ * h) ⁻¹' (↑K₀ : Set G)) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)
hm₁₁ 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) (g₁ : G)
    (hg₁ : g₁ ∈ s) (g₂ : G) (hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)),
    Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
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) (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₂)),
    Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
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) (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₂)),
    Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
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) (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₂
⊢ 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

Premises used: Set.iUnion₂_subset, MeasureTheory.Measure.haar.index_elim, mul_assoc, TopologicalSpace.PositiveCompacts.interior_nonempty, Set.mem_setOf_eq, Finset.card_mul_le, Nat.sInf_le, TopologicalSpace.Compacts.isCompact, mul_comm, TopologicalSpace.PositiveCompacts.isCompact, rfl, Set.mem_preimage, Set.preimage_subset_iff, le_trans