English
If b ∉ range(f.hom), then h(x) acting on the coset ⟨b•range, b⟩ yields the coset ⟨(x b)•range, x b⟩, i.e. h moves to the coset corresponding to xb.
Русский
Если b не принадлежит диапазону, то действие h(x) на косет ⟨b•range, b⟩ переходит к косету ⟨(x b)•range, x b⟩, то есть hb переводит на xb.
LaTeX
$$$$ h(x)\big(\mathrm{fromCoset}\langle b \operatorname{range}(f), b, rfl \rangle\big) = \mathrm{fromCoset}\langle (x b) \operatorname{range}(f), x b, rfl \rangle. $$$$
Lean4
theorem h_apply_fromCoset_nin_range (x : B) (hx : x ∈ f.hom.range) (b : B) (hb : b ∉ f.hom.range) :
h x (fromCoset ⟨b • f.hom.range, b, rfl⟩) = fromCoset ⟨(x * b) • ↑f.hom.range, x * b, rfl⟩ :=
by
change ((τ).symm.trans (g x)).trans τ _ = _
simp only [tau, Equiv.coe_trans, Function.comp_apply]
rw [Equiv.symm_swap,
@Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) ∞
(fromCoset ⟨b • ↑f.hom.range, b, rfl⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]
simp only [g_apply_fromCoset, leftCoset_assoc]
refine Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb ?_) (by simp)
convert Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r
rw [← mul_assoc, inv_mul_cancel, one_mul]
