English
Let f: F → M be a monoid hom and x,y ∈ Range(f). Then the number of g with f(g)=x equals the number with f(g)=y.
Русский
Пусть f: F → M — моноидный гомоморфизм и x,y ∈ Range(f). Тогда число g с f(g)=x равно числу g с f(g)=y.
LaTeX
$$#{g | f g = x} = #{g | f g = y}$$
Lean4
@[to_additive]
theorem 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} := by
rcases hx with ⟨x, rfl⟩
rcases hy with ⟨y, rfl⟩
rcases mul_left_surjective x y with ⟨y, rfl⟩
conv_lhs => rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]
congr 2 with g
simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]
let f' := MonoidHomClass.toMonoidHom f
change f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y
rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]
