English
The equality of the coe-smul' lemma: the coerced version of smul equals the explicit smulLeft map.
Русский
Неравенство/равенство коэрцированного smul' совпадает с явной картой smulLeft.
LaTeX
$$$ \text{coe\_smul'} = \text{smulLeft}$$$
Lean4
/-- The maximal element of every nonempty chain of `extension_of i f`. -/
def max {c : Set (ExtensionOf i f)} (hchain : IsChain (· ≤ ·) c) (hnonempty : c.Nonempty) : ExtensionOf i f :=
{
LinearPMap.sSup _
(IsChain.directedOn <|
chain_linearPMap_of_chain_extensionOf
hchain) with
le := by
refine
le_trans hnonempty.some.le <|
(LinearPMap.le_sSup _ <| (Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩).1
is_extension := fun m => by
refine Eq.trans (hnonempty.some.is_extension m) ?_
symm
generalize_proofs _ _ h1
exact
LinearPMap.sSup_apply (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
((Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩) ⟨i m, h1⟩ }
