-- Mathlib/GroupTheory/CosetCover.lean
theorem exists_index_le_card_of_leftCoset_cover :
    ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ 0 < ↑s.card

Tactic:
exact_mod_cast hs'

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
⊢ False

Tactic:
apply (one_le_sum_inv_index_of_leftCoset_cover hcovers).not_lt

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Proof state:
case inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
⊢ (↑(H i).index)⁻¹ < (↑s.card)⁻¹

Tactic:
rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Tactic:
apply (Finset.sum_lt_sum_of_nonempty hs hlt).trans_eq

Result:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹
⊢ ∑ i ∈ s, (↑s.card)⁻¹ = 1

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ ↑s.card < ↑(H i).index

Tactic:
exact_mod_cast h i hi ⟨hindex⟩

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ (↑(H i).index)⁻¹ < (↑s.card)⁻¹

Tactic:
exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹
⊢ ∑ i ∈ s, (↑s.card)⁻¹ = 1

Tactic:
rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
⊢ (↑(H i).index)⁻¹ < (↑s.card)⁻¹

Tactic:
cases eq_or_ne (H i).index 0 with
| inl hindex =>
  rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
| inr hindex =>
  exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Tactic:
have hs' : 0 < s.card := hs.card_pos

Result:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
⊢ ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

Tactic:
by_contra! h

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
⊢ False

Proof state:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Tactic:
have hlt : ∀ i ∈ s, ((H i).index : ℚ)⁻¹ < (s.card : ℚ)⁻¹ := fun i hi ↦ by
  cases eq_or_ne (H i).index 0 with
  | inl hindex =>
    rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
  | inr hindex =>
    exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)

Result:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Tactic:
cases s.eq_empty_or_nonempty with
| inl hs => simp only [hs, Finset.sum_empty, zero_lt_one]
| inr hs =>
have hs' : 0 < s.card := hs.card_pos
have hlt : ∀ i ∈ s, ((H i).index : ℚ)⁻¹ < (s.card : ℚ)⁻¹ := fun i hi ↦ by
  cases eq_or_ne (H i).index 0 with
  | inl hindex =>
    rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
  | inr hindex =>
    exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)
apply (Finset.sum_lt_sum_of_nonempty hs hlt).trans_eq
rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s = ∅
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Tactic:
simp only [hs, Finset.sum_empty, zero_lt_one]

Result:
no goals