G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this : Setoid G := QuotientGroup.leftRel H
⊢ index (comap f H) = index H
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
⊢ index (comap f H) = index H
letI := QuotientGroup.leftRel H
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ index (comap f H) = index H
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this : Setoid G := QuotientGroup.leftRel H
⊢ index (comap f H) = index H
letI := QuotientGroup.leftRel (H.comap f)
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))

case refine'_2
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Surjective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ index (comap f H) = index H
refine' Cardinal.toNat_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨_, _⟩)
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ ∀ (x y : G'), x⁻¹ * y ∈ comap f H ↔ (↑f x)⁻¹ * ↑f y ∈ H
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
simp only [QuotientGroup.leftRel_apply]
no goals
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
x y : G'
⊢ ↑f (x⁻¹ * y) = (↑f x)⁻¹ * ↑f y
rw [f.map_mul, f.map_inv]
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
simp_rw [← Quotient.eq''] at key
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄,
    Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
        Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a₂ →
      Quotient.mk'' x = a₂
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
refine' Quotient.ind' fun x => _
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x y : G'
⊢ Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
      Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' y) →
    Quotient.mk'' x = Quotient.mk'' y
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄,
    Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
        Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a₂ →
      Quotient.mk'' x = a₂
refine' Quotient.ind' fun y => _
no goals
case refine'_1
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x y : G'
⊢ Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
      Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' y) →
    Quotient.mk'' x = Quotient.mk'' y
exact (key x y).mpr
case refine'_2
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
case refine'_2
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Surjective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
refine' Quotient.ind' fun x => _
case refine'_2.intro
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
y : G'
hy : ↑f y = x
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
case refine'_2
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
obtain ⟨y, hy⟩ := hf x
no goals
case refine'_2.intro
G : Type u_2
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_1
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
y : G'
hy : ↑f y = x
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩