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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index 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)
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩
case 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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩
case 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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ Finset.card s + Finset.card t
case 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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
rw [← h2s, ← h2t]
case 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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ Finset.card (s ∪ t)
case 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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ Finset.card s + Finset.card t
refine' le_trans _ (Finset.card_union_le _ _)
case intro.intro.intro.intro.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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ Finset.card (s ∪ t) ∈ Finset.card '' {t | K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
case 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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ Finset.card (s ∪ t)
apply Nat.sInf_le
case intro.intro.intro.intro.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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ s ∪ t ∈ {t | K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
case intro.intro.intro.intro.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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ Finset.card (s ∪ t) ∈ Finset.card '' {t | K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
refine' ⟨_, _, rfl⟩
case intro.intro.intro.intro.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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s ∪ t), (fun h => g * h) ⁻¹' V
case intro.intro.intro.intro.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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ s ∪ t ∈ {t | K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
rw [mem_setOf_eq]
no goals
case intro.intro.intro.intro.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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ K₁.carrier ∪ K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ s ∪ t), (fun h => g * h) ⁻¹' V
apply union_subset <;> refine' Subset.trans (by assumption) _ <;>
  apply biUnion_subset_biUnion_left <;> intro g hg <;> simp only [mem_def] at hg <;>
  simp only [mem_def, Multiset.mem_union, Finset.union_val, hg, or_true_iff, true_or_iff]
no goals
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)
s : Finset G
h1s : K₁.carrier ⊆ ⋃ (g : G) (_ : g ∈ s), (fun h => g * h) ⁻¹' V
h2s : Finset.card s = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
h2t : Finset.card t = index K₂.carrier V
⊢ K₂.carrier ⊆ ?m.44697
assumption