-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
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
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
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),
    {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
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)
    (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})
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),
    ∀ x ∈ s,
      ((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty → ¬((fun (x_1 : G) ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty
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,
      ∀ (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
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,
      ∀ (g₂ : G) (h2g₂ : g₂ ∈ K₁.carrier) (g₃ : G) (h2g₃ : g₃ ∈ K₂.carrier) (h1g₃ : g₁ * g₃ ∈ V) (h1g₂ : g₁ * g₂ ∈ V),
        False
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,
      ∀ (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⁻¹
left :
  ∀ (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,
      ∀ (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₁⁻¹
right right₁ :
  ∀ (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,
      ∀ (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₁⁻¹
⊢ index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index 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]

Premises used: Iff.mpr, MeasureTheory.Measure.haar.index_elim, TopologicalSpace.Compacts.isCompact', Finset.disjoint_filter, Finset.filter_union_right, le_antisymm, inv_inv, mul_inv_rev, IsCompact.union, mul_inv_cancel_left, Finset.card_union_of_disjoint, Set.mem_preimage, Set.mem_mul, MeasureTheory.Measure.haar.index_union_le, Set.mem_inv