Lean4
/-- A copy of an `RCLike` field in which the `NormedField` field is adjusted to be become defeq
to a propeq one. -/
noncomputable def copy_of_normedField {𝕜 : Type*} (h : RCLike 𝕜) (hk : NormedField 𝕜) (h'' : hk = h.toNormedField) :
RCLike 𝕜 where
__ := hk
toPartialOrder := h.toPartialOrder
toDecidableEq := h.toDecidableEq
complete := by subst h''; exact h.complete
lt_norm_lt := by subst h''; exact h.lt_norm_lt
star := (@StarMul.toInvolutiveStar _ (_) (@StarRing.toStarMul _ (_) h.toStarRing)).star
star_involutive := by subst h''; exact h.star_involutive
star_mul := by subst h''; exact h.star_mul
star_add := by subst h''; exact h.star_add
smul := (@Algebra.toSMul _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)).smul
algebraMap :=
{ toFun := @Algebra.algebraMap _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)
map_one' := by subst h''; exact h.algebraMap.map_one'
map_mul' := by subst h''; exact h.algebraMap.map_mul'
map_zero' := by subst h''; exact h.algebraMap.map_zero'
map_add' := by subst h''; exact h.algebraMap.map_add' }
commutes' := by subst h''; exact h.commutes'
smul_def' := by subst h''; exact h.smul_def'
norm_smul_le := by subst h''; exact h.norm_smul_le
re := by subst h''; exact h.re
im := by subst h''; exact h.im
I := h.I
I_re_ax := by subst h''; exact h.I_re_ax
I_mul_I_ax := by subst h''; exact h.I_mul_I_ax
re_add_im_ax := by subst h''; exact h.re_add_im_ax
ofReal_re_ax := by subst h''; exact h.ofReal_re_ax
ofReal_im_ax := by subst h''; exact h.ofReal_im_ax
mul_re_ax := by subst h''; exact h.mul_re_ax
mul_im_ax := by subst h''; exact h.mul_im_ax
conj_re_ax := by subst h''; exact h.conj_re_ax
conj_im_ax := by subst h''; exact h.conj_im_ax
conj_I_ax := by subst h''; exact h.conj_I_ax
norm_sq_eq_def_ax := by subst h''; exact h.norm_sq_eq_def_ax
mul_im_I_ax := by subst h''; exact h.mul_im_I_ax
le_iff_re_im := by subst h''; exact h.le_iff_re_im
