-- Mathlib/GroupTheory/Complement.lean
/-- Given two subgroups `H' ⊆ H`, there exists a left transversal to `H'` inside `H`. -/
@[to_additive "Given two subgroups `H' ⊆ H`, there exists a transversal to `H'` inside `H`"]
lemma exists_left_transversal_of_le {H' H : Subgroup G} (h : H' ≤ H) :
    ∃ S : Set G, S * H' = H ∧ Nat.card S * Nat.card H' = Nat.card H

Proof state:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ H' = map H.subtype H''

Tactic:
simp [H'', h]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ ∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Tactic:
refine ⟨H.subtype '' S, ?_, ?_⟩

Result:
case intro.intro.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ ⇑H.subtype '' S * ↑(map H.subtype H'') = ↑H

case intro.intro.refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Proof state:
case intro.intro.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' univ = ↑H

Tactic:
simp [Set.ext_iff]

Result:
no goals

Proof state:
case intro.intro.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' S * ↑(map H.subtype H'') = ↑H

Tactic:
rw [← this, cmem.mul_eq]

Result:
case intro.intro.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' univ = ↑H

Proof state:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Tactic:
rw [this]

Result:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Proof state:
case intro.intro.refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Tactic:
rw [← cmem.card_mul_card]

Result:
case intro.intro.refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) * Nat.card ↥(map H.subtype H'') = Nat.card ↑S * Nat.card ↑↑H''

Proof state:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Tactic:
obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_left 1

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ ∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Proof state:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Tactic:
let H'' : Subgroup H := H'.comap H.subtype

Result:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Proof state:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Tactic:
have : H' = H''.map H.subtype := by simp [H'', h]

Result:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Proof state:
case intro.intro.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ ⇑H.subtype '' S * ↑(map H.subtype H'') = ↑H

Tactic:
have : H.subtype '' (S * H'') = H.subtype '' S * H''.map H.subtype := image_mul H.subtype

Result:
case intro.intro.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' S * ↑(map H.subtype H'') = ↑H