G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
⊢ index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V
apply le_antisymm (index_union_le K₁ K₂ hV)
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
⊢ index K₁.carrier V + index K₂.carrier V ≤ Finset.card s
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
⊢ index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
rw [← h2s]
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₁.carrier)) s) +
      Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₂.carrier)) s) ≤
    Finset.card s
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ index K₁.carrier V + index K₂.carrier V ≤ Finset.card s
refine'
  le_trans
    (add_le_add (this K₁.1 <| Subset.trans (subset_union_left _ _) h1s)
      (this K₂.1 <| Subset.trans (subset_union_right _ _) h1s)) _
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Finset.card
      (Finset.filter
        (fun x =>
          Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₁.carrier) ∨ Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₂.carrier))
        s) ≤
    Finset.card s

case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Disjoint (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₁.carrier)) s)
    (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₂.carrier)) s)
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₁.carrier)) s) +
      Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₂.carrier)) s) ≤
    Finset.card s
rw [← Finset.card_union_eq, Finset.filter_union_right]
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Disjoint (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₁.carrier)) s)
    (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₂.carrier)) s)
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Finset.card
      (Finset.filter
        (fun x =>
          Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₁.carrier) ∨ Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₂.carrier))
        s) ≤
    Finset.card s

case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Disjoint (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₁.carrier)) s)
    (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₂.carrier)) s)
exact s.card_filter_le _
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ ∀ (x : G),
    x ∈ s → Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₁.carrier) → ¬Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₂.carrier)
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ Disjoint (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₁.carrier)) s)
    (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K₂.carrier)) s)
apply Finset.disjoint_filter.mpr
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h1g₂ : g₂ ∈ (fun h => g₁ * h) ⁻¹' V
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h1g₃ : g₃ ∈ (fun h => g₁ * h) ⁻¹' V
h2g₃ : g₃ ∈ K₂.carrier
⊢ False
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
⊢ ∀ (x : G),
    x ∈ s → Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₁.carrier) → ¬Set.Nonempty ((fun h => x * h) ⁻¹' V ∩ K₂.carrier)
rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ False
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h1g₂ : g₂ ∈ (fun h => g₁ * h) ⁻¹' V
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h1g₃ : g₃ ∈ (fun h => g₁ * h) ⁻¹' V
h2g₃ : g₃ ∈ K₂.carrier
⊢ False
simp only [mem_preimage] at h1g₃ h1g₂
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : 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⁻¹
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ False
refine' h.le_bot (_ : g₁⁻¹ ∈ _)
case intro.intro.intro.intro.intro.intro.left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x, x ∈ K₁.carrier ∧ ∃ x_1, x_1⁻¹ ∈ V ∧ x * x_1 = g₁⁻¹

case intro.intro.intro.intro.intro.intro.right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x, x ∈ K₂.carrier ∧ ∃ x_1, x_1⁻¹ ∈ V ∧ x * x_1 = g₁⁻¹
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : 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⁻¹
constructor <;> simp only [Set.mem_inv, Set.mem_mul, exists_exists_and_eq_and, exists_and_left]
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
⊢ ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
intro K hK
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s) ∈
    Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
apply Nat.sInf_le
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s ∈
    {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s) ∈
    Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
refine' ⟨_, _, rfl⟩
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ K ⊆ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s ∈
    {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
rw [mem_setOf_eq]
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
⊢ g ∈ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
⊢ K ⊆ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
intro g hg
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g ∈ (fun h => (fun h => g₀ * h) ⁻¹' V) h1g₀
⊢ g ∈ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
case hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
⊢ g ∈ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
rcases hK hg with ⟨_, ⟨g₀, rfl⟩, _, ⟨h1g₀, rfl⟩, h2g₀⟩
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g ∈ (fun h => (fun h => g₀ * h) ⁻¹' V) h1g₀
⊢ g ∈ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
simp only [mem_preimage] at h2g₀
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ ∃ i i_1, g ∈ (fun h => i * h) ⁻¹' V
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ ⋃ (g : G) (_ : g ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s), (fun h => g * h) ⁻¹' V
simp only [mem_iUnion]
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ ∃ i, g ∈ (fun h => g₀ * h) ⁻¹' V
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ ∃ i i_1, g ∈ (fun h => i * h) ⁻¹' V
use g₀
case hm.intro.intro.intro.intro.intro.intro.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h => g₀ * h) ⁻¹' V

case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g₀ ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s
case hm.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ ∃ i, g ∈ (fun h => g₀ * h) ⁻¹' V
constructor
case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g₀ ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s

case hm.intro.intro.intro.intro.intro.intro.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h => g₀ * h) ⁻¹' V
case hm.intro.intro.intro.intro.intro.intro.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h => g₀ * h) ⁻¹' V

case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g₀ ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s
swap
no goals
case hm.intro.intro.intro.intro.intro.intro.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h => g₀ * h) ⁻¹' V
exact h2g₀
case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ Set.Nonempty ((fun h => g₀ * h) ⁻¹' V ∩ K)
case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g₀ ∈ Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s
simp only [Finset.mem_filter, h1g₀, true_and_iff]
case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h => g₀ * h) ⁻¹' V ∩ K
case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ Set.Nonempty ((fun h => g₀ * h) ⁻¹' V ∩ K)
use g
no goals
case hm.intro.intro.intro.intro.intro.intro.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h => g₀ * h) ⁻¹' V ∩ K
simp only [hg, h2g₀, mem_inter_iff, mem_preimage, and_self_iff]
case intro.intro.intro.intro.intro.intro.left.refine'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₂)⁻¹⁻¹ ∈ V

case intro.intro.intro.intro.intro.intro.left.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₂ * (g₁ * g₂)⁻¹ = g₁⁻¹
case intro.intro.intro.intro.intro.intro.left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x, x ∈ K₁.carrier ∧ ∃ x_1, x_1⁻¹ ∈ V ∧ x * x_1 = g₁⁻¹
refine' ⟨_, h2g₂, (g₁ * g₂)⁻¹, _, _⟩
case intro.intro.intro.intro.intro.intro.left.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₂ * (g₁ * g₂)⁻¹ = g₁⁻¹
case intro.intro.intro.intro.intro.intro.left.refine'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₂)⁻¹⁻¹ ∈ V

case intro.intro.intro.intro.intro.intro.left.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₂ * (g₁ * g₂)⁻¹ = g₁⁻¹
simp only [inv_inv, h1g₂]
no goals
case intro.intro.intro.intro.intro.intro.left.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₂ * (g₁ * g₂)⁻¹ = g₁⁻¹
simp only [mul_inv_rev, mul_inv_cancel_left]
case intro.intro.intro.intro.intro.intro.right.refine'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₃)⁻¹⁻¹ ∈ V

case intro.intro.intro.intro.intro.intro.right.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹
case intro.intro.intro.intro.intro.intro.right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x, x ∈ K₂.carrier ∧ ∃ x_1, x_1⁻¹ ∈ V ∧ x * x_1 = g₁⁻¹
refine' ⟨_, h2g₃, (g₁ * g₃)⁻¹, _, _⟩
case intro.intro.intro.intro.intro.intro.right.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹
case intro.intro.intro.intro.intro.intro.right.refine'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₃)⁻¹⁻¹ ∈ V

case intro.intro.intro.intro.intro.intro.right.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹
simp only [inv_inv, h1g₃]
no goals
case intro.intro.intro.intro.intro.intro.right.refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : Set.Nonempty (interior V)
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G),
    (K ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V) →
      index K V ≤ Finset.card (Finset.filter (fun g => Set.Nonempty ((fun h => g * h) ⁻¹' V ∩ K)) s)
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹
simp only [mul_inv_rev, mul_inv_cancel_left]