English
The range of f.hom equals the set of elements x ∈ B for which h(x) = g(x); i.e. Range(f.hom) = { x | h(x) = g(x) }.
Русский
Образ f.hom равен множеству элементов x ∈ B, для которых выполняется h(x) = g(x); то есть Range(f.hom) = { x | h(x) = g(x) }.
LaTeX
$$$$ f.hom.range = \{ x \mid h(x) = g(x) \}. $$$$
Lean4
theorem agree : f.hom.range = {x | h x = g x} :=
by
refine Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩
· rintro ⟨a, rfl⟩
change h (f a) = g (f a)
ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
· rw [g_apply_fromCoset]
by_cases m : y ∈ f.hom.range
· rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
change fromCoset _ = fromCoset ⟨f a • (y • _), _⟩
simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]
· rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
simp only [leftCoset_assoc]
· rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
· have eq1 : (h b) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ :=
by
change ((τ).symm.trans (g b)).trans τ _ = _
dsimp [tau]
simp [g_apply_infinity f]
have eq2 : g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ := rfl
exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, DFunLike.congr_fun hb])
