-- Mathlib/GroupTheory/Schreier.lean
theorem exists_finset_card_le_mul [FiniteIndex H] {S : Finset G} (hS : closure (S : Set G) = ⊤) :
    ∃ T : Finset H, T.card ≤ H.index * S.card ∧ closure (T : Set H) = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
⊢ 1 ∈ R

Tactic:
rwa [Set.mem_toFinset]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
letI := H.fintypeQuotientOfFiniteIndex

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
replace hR1 : (1 : G) ∈ R := by rwa [Set.mem_toFinset]

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
haveI : DecidableEq G := Classical.decEq G

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this : DecidableEq G
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this : DecidableEq G
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
obtain ⟨R₀, hR, hR1⟩ := H.exists_isComplement_right 1

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
⊢ R.card = H.index

Tactic:
calc
  R.card = Fintype.card R := (Fintype.card_coe R).symm
  _ = _ := (Fintype.card_congr hR.rightQuotientEquiv).symm
  _ = Fintype.card (G ⧸ H) := QuotientGroup.card_quotient_rightRel H
  _ = H.index := by rw [index_eq_card, Nat.card_eq_fintype_card]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
refine ⟨_, ?_, closure_mul_image_eq_top' hR hR1 hS⟩

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
⊢ (Finset.image (fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)).card ≤ H.index * S.card

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
⊢ IsComplement ↑H ↑R

Tactic:
rwa [Set.coe_toFinset]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
let R : Finset G := Set.toFinset R₀

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
replace hR : IsComplement (H : Set G) R := by rwa [Set.coe_toFinset]

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
⊢ Fintype.card (G ⧸ H) = H.index

Tactic:
rw [index_eq_card, Nat.card_eq_fintype_card]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

Tactic:
haveI : Fintype R₀ := Fintype.ofEquiv _ hR.rightQuotientEquiv

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
⊢ ∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤