-- 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}
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)
⊢ 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),
  (↑K : Set G) ⊆ ⋃ g ∈ t * s, (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