-- Mathlib/GroupTheory/Index.lean
theorem index_comap_of_surjective {f : G' →* G} (hf : Function.Surjective f) :
    (H.comap f).index = H.index

Proof state:
case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
x : G
⊢ ∃ a, Quotient.map' ⇑f ⋯ a = Quotient.mk'' x

Tactic:
obtain ⟨y, hy⟩ := hf x

Result:
case refine_2.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
x : G
y : G'
hy : f y = x
⊢ ∃ a, Quotient.map' ⇑f ⋯ a = Quotient.mk'' x

Proof state:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (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 ⋯)

Tactic:
refine Quotient.ind' fun x => ?_

Result:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (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 ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ a₂ → Quotient.mk'' x = a₂

Proof state:
case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Function.Surjective (Quotient.map' ⇑f ⋯)

Tactic:
refine Quotient.ind' fun x => ?_

Result:
case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
x : G
⊢ ∃ a, Quotient.map' ⇑f ⋯ a = Quotient.mk'' x

Proof state:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Function.Injective (Quotient.map' ⇑f ⋯)

Tactic:
simp_rw [← Quotient.eq''] at key

Result:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (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 ⋯)

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
⊢ ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)

Tactic:
simp only [QuotientGroup.leftRel_apply]

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
⊢ ∀ (x y : G'), x⁻¹ * y ∈ comap f H ↔ (f x)⁻¹ * f y ∈ H

Proof state:
case refine_2.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
x : G
y : G'
hy : f y = x
⊢ ∃ a, Quotient.map' ⇑f ⋯ a = Quotient.mk'' x

Tactic:
exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩

Result:
no goals

Proof state:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (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 ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ a₂ → Quotient.mk'' x = a₂

Tactic:
refine Quotient.ind' fun y => ?_

Result:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (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 ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ (Quotient.mk'' y) → Quotient.mk'' x = Quotient.mk'' y

Proof state:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (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 ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ (Quotient.mk'' y) → Quotient.mk'' x = Quotient.mk'' y

Tactic:
exact (key x y).mpr

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ (comap f H).index = H.index

Tactic:
refine Cardinal.toNat_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)

Result:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Function.Injective (Quotient.map' ⇑f ⋯)

case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Function.Surjective (Quotient.map' ⇑f ⋯)

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Function.Surjective ⇑f
x y : G'
⊢ f (x⁻¹ * y) = (f x)⁻¹ * f y

Tactic:
rw [f.map_mul, f.map_inv]

Result:
no goals