-- Mathlib/GroupTheory/CosetCover.lean
theorem pairwiseDisjoint_leftCoset_cover_const_of_index_eq (hind : H.index = s.card) :
    Set.PairwiseDisjoint s (g · • (H : Set G))

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : ¬⟨i, hi⟩ = ⟨j, hj⟩
c : Set G
x : G
hx : x ∈ c
hi' : ↑(g i) = ↑x
hj' : ↑(g j) = ↑x
⊢ ↑(g ↑⟨i, hi⟩) = ↑(g ↑⟨j, hj⟩)

Tactic:
simp only [hi', hj']

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
⊢ (↑s).PairwiseDisjoint fun x => g x • ↑H

Tactic:
have : Fintype (G ⧸ H) := fintypeOfIndexNeZero fun h => by
  rw [hind, Finset.card_eq_zero] at h
  rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
  exact Set.empty_ne_univ hcovers

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ (↑s).PairwiseDisjoint fun x => g x • ↑H

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : ¬⟨i, hi⟩ = ⟨j, hj⟩
c : Set G
x : G
hx : x ∈ c
hi' : ↑(g i) = ↑x
hj' : ↑(g j) = ↑x
⊢ x ∈ ⊥

Tactic:
exact h' <| this.injective <| by simp only [hi', hj']

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
hj' : c ≤ (fun x => g x • ↑H) j
x : G
hx : x ∈ c
hi' : x ∈ (fun x => g x • ↑H) i
⊢ x ∈ ⊥

Tactic:
specialize hj' hx

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
x : G
hx : x ∈ c
hi' : x ∈ (fun x => g x • ↑H) i
hj' : x ∈ (fun x => g x • ↑H) j
⊢ x ∈ ⊥

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

Tactic:
rw [hind, Finset.card_eq_zero] at h

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

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ∅ = Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False

Tactic:
exact Set.empty_ne_univ hcovers

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
hi' : c ≤ (fun x => g x • ↑H) i
hj' : c ≤ (fun x => g x • ↑H) j
x : G
hx : x ∈ c
⊢ x ∈ ⊥

Tactic:
specialize hi' hx

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
hj' : c ≤ (fun x => g x • ↑H) j
x : G
hx : x ∈ c
hi' : x ∈ (fun x => g x • ↑H) i
⊢ x ∈ ⊥

Proof state:
case left
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Surjective fun x => ↑(g ↑x)

Tactic:
rwa [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers

Result:
no goals

Proof state:
case right
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Fintype.card { x // x ∈ s } = Fintype.card (G ⧸ H)

Tactic:
simp only [Fintype.card_coe, ← hind, index_eq_card, Nat.card_eq_fintype_card]

Result:
no goals

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

Tactic:
rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ∅ = Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
⊢ (↑s).PairwiseDisjoint fun x => g x • ↑H

Tactic:
intro i hi j hj h' c hi' hj' x hx

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
hi' : c ≤ (fun x => g x • ↑H) i
hj' : c ≤ (fun x => g x • ↑H) j
x : G
hx : x ∈ c
⊢ x ∈ ⊥

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Bijective fun x => ↑(g ↑x)

Tactic:
rw [Fintype.bijective_iff_surjective_and_card]

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ (Function.Surjective fun x => ↑(g ↑x)) ∧ Fintype.card { x // x ∈ s } = Fintype.card (G ⧸ H)

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
x : G
hx : x ∈ c
hi' : x ∈ (fun x => g x • ↑H) i
hj' : x ∈ (fun x => g x • ↑H) j
⊢ x ∈ ⊥

Tactic:
rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x => ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
x : G
hx : x ∈ c
hi' : ↑(g i) = ↑x
hj' : ↑(g j) = ↑x
⊢ x ∈ ⊥

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ (Function.Surjective fun x => ↑(g ↑x)) ∧ Fintype.card { x // x ∈ s } = Fintype.card (G ⧸ H)

Tactic:
constructor

Result:
case left
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Surjective fun x => ↑(g ↑x)

case right
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Fintype.card { x // x ∈ s } = Fintype.card (G ⧸ H)