-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma card_fiber_eq_of_mem_range (f : F) {x y : M} (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) :
    #{g | f g = x} = #{g | f g = y}

Proof state:
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : M
hx : x ∈ Set.range ⇑f
hy : y ∈ Set.range ⇑f
⊢ #(filter (fun g => f g = x) univ) = #(filter (fun g => f g = y) univ)

Tactic:
rcases hx with ⟨x, rfl⟩

Result:
case intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
y : M
hy : y ∈ Set.range ⇑f
x : G
⊢ #(filter (fun g => f g = f x) univ) = #(filter (fun g => f g = y) univ)

Proof state:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y

Tactic:
rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]

Result:
no goals

Proof state:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
⊢ f g * f y⁻¹ = f x ↔ f g = f x * f y

Tactic:
let f' := MonoidHomClass.toMonoidHom f

Result:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f g * f y⁻¹ = f x ↔ f g = f x * f y

Proof state:
case intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
y : M
hy : y ∈ Set.range ⇑f
x : G
⊢ #(filter (fun g => f g = f x) univ) = #(filter (fun g => f g = y) univ)

Tactic:
rcases hy with ⟨y, rfl⟩

Result:
case intro.intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #(filter (fun g => f g = f x) univ) = #(filter (fun g => f g = f y) univ)

Proof state:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
⊢ ((fun g => f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) g ↔ f g = f ((fun x_1 => x * x_1) y)

Tactic:
simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]

Result:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
⊢ f g * f y⁻¹ = f x ↔ f g = f x * f y

Proof state:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f g * f y⁻¹ = f x ↔ f g = f x * f y

Tactic:
show f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y

Result:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y

Proof state:
case intro.intro.intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #(filter (fun g => f g = f x) univ) = #(filter (fun g => f g = f ((fun x_1 => x * x_1) y)) univ)

Tactic:
conv_lhs =>
  rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]

Result:
case intro.intro.intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #(filter ((fun g => f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) univ) =
    #(filter (fun g => f g = f ((fun x_1 => x * x_1) y)) univ)

Proof state:
case intro.intro.intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #(filter ((fun g => f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) univ) =
    #(filter (fun g => f g = f ((fun x_1 => x * x_1) y)) univ)

Tactic:
congr 2 with g

Result:
case intro.intro.intro.e_s.e_p.h.a
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
⊢ ((fun g => f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) g ↔ f g = f ((fun x_1 => x * x_1) y)

Proof state:
case intro.intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #(filter (fun g => f g = f x) univ) = #(filter (fun g => f g = f y) univ)

Tactic:
rcases mul_left_surjective x y with ⟨y, rfl⟩

Result:
case intro.intro.intro
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #(filter (fun g => f g = f x) univ) = #(filter (fun g => f g = f ((fun x_1 => x * x_1) y)) univ)