Lean4
/-- The additive equivalence between `Quot F` and `Quot (F ⋙ uliftFunctor.{u'})`.
-/
@[simp]
def quotQuotUliftAddEquiv [DecidableEq J] : Quot F ≃+ Quot (F ⋙ uliftFunctor.{u'})
where
toFun := quotToQuotUlift F
invFun := quotUliftToQuot F
left_inv
x := by
conv_rhs => rw [← AddMonoidHom.id_apply _ x]
rw [← AddMonoidHom.comp_apply,
Quot.addMonoidHom_ext F (f := (quotUliftToQuot F).comp (quotToQuotUlift F)) (fun j a ↦ ?_)]
rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotToQuotUlift_ι, quotUliftToQuot_ι]
right_inv
x := by
conv_rhs => rw [← AddMonoidHom.id_apply _ x]
rw [← AddMonoidHom.comp_apply,
Quot.addMonoidHom_ext _ (f := (quotToQuotUlift F).comp (quotUliftToQuot F)) (fun j a ↦ ?_)]
rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotUliftToQuot_ι, quotToQuotUlift_ι]
rfl
map_add' _ _ := by simp
