[Merged by Bors] - chore(Algebra/Order/Hom/Basic): remove outParam

[riccardobrasca]

Remove unedeed outParam.

[riccardobrasca]

I have no idea why I cannot remove more outParam. For example, if I remove the second outParam in

/-- `NonArchimedeanHomClass F α β` states that `F` is a type of non-archimedean morphisms. -/
class NonArchimedeanHomClass (F : Type _) (α β : outParam (Type _)) [outParam (Add α)]
  [outParam (LinearOrder β)] extends FunLike F α fun _ => β where
  /-- the image of a sum is less or equal than the maximum of the images. -/
  map_add_le_max (f : F) : ∀ a b, f (a + b) ≤ max (f a) (f b)

I get an error ("function expected at f term has type F") in

@[to_additive]
theorem le_map_mul_map_div [Group α] [CommSemigroup β] [LE β] [SubMultiplicativeHomClass F α β]
    (f : F) (a b : α) : f a ≤ f b * f (a / b) := by
  simpa only [mul_comm, div_mul_cancel'] using map_mul_le_mul f (a / b) b

even if this theorem seems unrelated to NonArchimedeanHomClass.

[kim-em]

@riccardobrasca, let's merge what can be merged for now. Can you post on zulip with the error? If you feel like trying to minimize it that would be helpful. Quite possibly this is a Lean 4 bug.

[kim-em]

Okay, I have minimised this to:

class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

instance (priority := 100) {F α β} [FunLike F α β] : CoeFun F fun _ => ∀ a : α, β a where coe := FunLike.coe

structure A (α : Type u) where

class S (F : Type _) (α β : outParam (Type _)) extends FunLike F α fun _ => β where

-- Comment out either this instance or this class, and the error goes away.
instance {α} [Add α] : Add (A α) := sorry
-- Replacing `[Add α]` with `[outParam (Add α)]` also kills the error.
class T (F : Type _) (α β : outParam (Type _)) [Add α] extends FunLike F α fun _ => β where

-- Errors with `function expected at f term has type F`:
example [S F α β] (f : F) (a b : α) : f a = f b := by
  sorry

I'll pursue it on zulip.

[kim-em]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style