case intro
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
y : H
hy : y ∈ Set.range ↑f
x : G
⊢ card (filter (fun g => ↑f g = ↑f x) univ) = card (filter (fun g => ↑f g = y) univ)
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : H
hx : x ∈ Set.range ↑f
hy : y ∈ Set.range ↑f
⊢ card (filter (fun g => ↑f g = x) univ) = card (filter (fun g => ↑f g = y) univ)
rcases hx with ⟨x, rfl⟩
case intro.intro
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ card (filter (fun g => ↑f g = ↑f x) univ) = card (filter (fun g => ↑f g = ↑f y) univ)
case intro
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
y : H
hy : y ∈ Set.range ↑f
x : G
⊢ card (filter (fun g => ↑f g = ↑f x) univ) = card (filter (fun g => ↑f g = y) univ)
rcases hy with ⟨y, rfl⟩
case intro.intro.refine'_1
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a : G) (ha : a ∈ filter (fun g => ↑f g = ↑f x) univ),
    (fun g x_1 => g * x⁻¹ * y) a ha ∈ filter (fun g => ↑f g = ↑f y) univ

case intro.intro.refine'_2
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a b : G) (ha : a ∈ filter (fun g => ↑f g = ↑f x) univ) (hb : b ∈ filter (fun g => ↑f g = ↑f x) univ),
    (fun g x_1 => g * x⁻¹ * y) a ha = (fun g x_1 => g * x⁻¹ * y) b hb → a = b

case intro.intro.refine'_3
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : g ∈ filter (fun g => ↑f g = ↑f y) univ
⊢ ∃ ha, (fun g x_1 => g * x⁻¹ * y) (g * y⁻¹ * x) ha = g
case intro.intro
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ card (filter (fun g => ↑f g = ↑f x) univ) = card (filter (fun g => ↑f g = ↑f y) univ)
refine' card_congr (fun g _ => g * x⁻¹ * y) _ _ fun g hg => ⟨g * y⁻¹ * x, _⟩
case intro.intro.refine'_1
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a : G), True ∧ ↑f a = ↑f x → True ∧ ↑f x * ↑f x⁻¹ * ↑f y = ↑f y
case intro.intro.refine'_1
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a : G) (ha : a ∈ filter (fun g => ↑f g = ↑f x) univ),
    (fun g x_1 => g * x⁻¹ * y) a ha ∈ filter (fun g => ↑f g = ↑f y) univ
simp (config := { contextual := true }) only [*, mem_filter, one_mul, MonoidHom.map_mul,
  mem_univ, mul_right_inv, eq_self_iff_true, MonoidHom.map_mul_inv, and_self_iff,
  forall_true_iff]
no goals
case intro.intro.refine'_1
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a : G), True ∧ ↑f a = ↑f x → True ∧ ↑f x * ↑f x⁻¹ * ↑f y = ↑f y
simp only [true_and, map_inv, mul_right_inv, one_mul, and_self, implies_true, forall_const]
no goals
case intro.intro.refine'_2
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a b : G) (ha : a ∈ filter (fun g => ↑f g = ↑f x) univ) (hb : b ∈ filter (fun g => ↑f g = ↑f x) univ),
    (fun g x_1 => g * x⁻¹ * y) a ha = (fun g x_1 => g * x⁻¹ * y) b hb → a = b
simp only [mul_left_inj, imp_self, forall₂_true_iff]
case intro.intro.refine'_3
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : ↑f g = ↑f y
⊢ ∃ ha, (fun g x_1 => g * x⁻¹ * y) (g * y⁻¹ * x) ha = g
case intro.intro.refine'_3
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : g ∈ filter (fun g => ↑f g = ↑f y) univ
⊢ ∃ ha, (fun g x_1 => g * x⁻¹ * y) (g * y⁻¹ * x) ha = g
simp only [true_and_iff, mem_filter, mem_univ] at hg
case intro.intro.refine'_3
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : ↑f g = ↑f y
⊢ ∃ h, True
case intro.intro.refine'_3
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : ↑f g = ↑f y
⊢ ∃ ha, (fun g x_1 => g * x⁻¹ * y) (g * y⁻¹ * x) ha = g
simp only [hg, mem_filter, one_mul, MonoidHom.map_mul, mem_univ, mul_right_inv,
  eq_self_iff_true, exists_prop_of_true, MonoidHom.map_mul_inv, and_self_iff,
  mul_inv_cancel_right, inv_mul_cancel_right]
no goals
case intro.intro.refine'_3
R : Type ?u.416251
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_1
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : ↑f g = ↑f y
⊢ ∃ h, True
simp only [map_inv, mul_right_inv, one_mul, and_self, exists_prop]