minimising Oliver's simp example

example.lean

set_option autoImplicit true

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
  one := 1

class MulZeroClass (M₀ : Type _) extends Mul M₀, Zero M₀ where
  zero_mul : ∀ a : M₀, 0 * a = 0
  mul_zero : ∀ a : M₀, a * 0 = 0

class AddSemigroup (G : Type u) extends Add G where
  add_assoc : ∀ a b c : G, a + b + c = a + (b + c)

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a

class AddCommSemigroup (G : Type u) extends AddSemigroup G where
  add_comm : ∀ a b : G, a + b = b + a

class SemigroupWithZero (S₀ : Type _) extends Semigroup S₀, MulZeroClass S₀

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

class AddZeroClass (M : Type u) extends Zero M, Add M where
  zero_add : ∀ a : M, 0 + a = a
  add_zero : ∀ a : M, a + 0 = a

class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀

class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where

class Monoid (M : Type u) extends Semigroup M, MulOneClass M where

structure Units (α : Type u) [Monoid α] where
  val : α
  inv : α
  val_inv : val * inv = 1
  inv_val : inv * val = 1

postfix:1024 "ˣ" => Units

class Inv (α : Type u) where
  inv : α → α

postfix:max "⁻¹" => Inv.inv

instance [Monoid α] : Inv αˣ :=
  ⟨fun u => ⟨u.2, u.1, u.4, u.3⟩⟩

instance [Monoid α] : CoeHead αˣ α :=
  ⟨Units.val⟩

def divp [Monoid α] (a : α) (u : Units α) : α :=
  a * (u⁻¹ : αˣ)

infixl:70 " /ₚ " => divp

class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀

class LeftCancelSemigroup (G : Type u) extends Semigroup G where
  mul_left_cancel : ∀ a b c : G, a * b = a * c → b = c

class LeftCancelMonoid (M : Type u) extends LeftCancelSemigroup M, Monoid M

class RightCancelSemigroup (G : Type u) extends Semigroup G where
  mul_right_cancel : ∀ a b c : G, a * b = c * b → a = c

class RightCancelMonoid (M : Type u) extends RightCancelSemigroup M, Monoid M

class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M

class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
  sub a b := a + -b
  sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl

class AddGroup (A : Type u) extends SubNegMonoid A where
  add_left_neg : ∀ a : A, -a + a = 0

class AddMonoidWithOne (R : Type u) extends AddMonoid R, One R where

class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M

class AddGroupWithOne (R : Type u) extends AddMonoidWithOne R, AddGroup R where

class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G

class Distrib (R : Type _) extends Mul R, Add R where
  protected left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  protected right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α

class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α

class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α

class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α

class CommSemiring (R : Type u) extends Semiring R, CommMonoid R

class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R

class CommRing (α : Type u) extends Ring α, CommMonoid α

section RingHom

def Function.Injective (f : α → β) : Prop :=
  ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂


class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  /-- The coercion from `F` to a function. -/
  coe : F → ∀ a : α, β a
  /-- The coercion to functions must be injective. -/
  coe_injective' : Function.Injective coe

section Dependent

/-! ### `FunLike F α β` where `β` depends on `a : α` -/

variable (F α : Sort _) (β : α → Sort _)

namespace FunLike

variable {F α β} [i : FunLike F α β]

instance (priority := 100) hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

-- #eval Lean.Elab.Command.liftTermElabM do
--   Std.Tactic.Coe.registerCoercion ``FunLike.coe
--     (some { numArgs := 5, coercee := 4, type := .coeFun })

end FunLike

end Dependent

structure ZeroHom (M : Type _) (N : Type _) [Zero M] [Zero N] where
  /-- The underlying function -/
  toFun : M → N
  /-- The proposition that the function preserves 0 -/
  map_zero' : toFun 0 = 0

class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N]
  extends FunLike F M fun _ => N where
  /-- The proposition that the function preserves 0 -/
  map_zero : ∀ f : F, f 0 = 0

instance ZeroHom.zeroHomClass {M N : Type _} [Zero M] [Zero N] : ZeroHomClass (ZeroHom M N) M N where
  coe := ZeroHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
  map_zero := ZeroHom.map_zero'

def ZeroHomClass.toZeroHom {M N F : Type _} [Zero M] [Zero N] [ZeroHomClass F M N] (f : F) : ZeroHom M N where
  toFun := f
  map_zero' := map_zero f

instance {M N F : Type _} [Zero M] [Zero N] [ZeroHomClass F M N] : CoeTC F (ZeroHom M N) :=
  ⟨ZeroHomClass.toZeroHom⟩

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
  /-- The underlying function -/
  toFun : M → N
  /-- The proposition that the function preserves 1 -/
  map_one' : toFun 1 = 1

class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
  extends FunLike F M fun _ => N where
  /-- The proposition that the function preserves 1 -/
  map_one : ∀ f : F, f 1 = 1

instance OneHom.oneHomClass {M N : Type _} [One M] [One N] : OneHomClass (OneHom M N) M N where
  coe := OneHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
  map_one := OneHom.map_one'

/-- Turn an element of a type `F` satisfying `OneHomClass F M N` into an actual
`OneHom`. This is declared as the default coercion from `F` to `OneHom M N`. -/
def OneHomClass.toOneHom {M N F : Type _} [One M] [One N] [OneHomClass F M N] (f : F) : OneHom M N where
  toFun := f
  map_one' := map_one f

/-- Any type satisfying `OneHomClass` can be cast into `OneHom` via `OneHomClass.toOneHom`. -/
instance {M N F : Type _} [One M] [One N] [OneHomClass F M N] : CoeTC F (OneHom M N) :=
  ⟨OneHomClass.toOneHom⟩

structure AddHom (M : Type _) (N : Type _) [Add M] [Add N] where
  /-- The underlying function -/
  toFun : M → N
  /-- The proposition that the function preserves addition -/
  map_add' : ∀ x y, toFun (x + y) = toFun x + toFun y

class AddHomClass (F : Type _) (M N : outParam (Type _)) [Add M] [Add N]
  extends FunLike F M fun _ => N where
  /-- The proposition that the function preserves addition -/
  map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y

instance AddHom.addHomClass {M N : Type _} [Add M] [Add N] : AddHomClass (AddHom M N) M N where
  coe := AddHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
  map_add := AddHom.map_add'

def AddHomClass.toAddHom {M N F : Type _} [Add M] [Add N] [AddHomClass F M N] (f : F) : AddHom M N where
  toFun := f
  map_add' := map_add f

instance {M N F : Type _} [Add M] [Add N] [AddHomClass F M N] : CoeTC F (AddHom M N) :=
  ⟨AddHomClass.toAddHom⟩

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
  toFun : M → N
  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

/-- `M →ₙ* N` denotes the type of multiplication-preserving maps from `M` to `N`. -/
infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]
  extends FunLike F M fun _ => N where
  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

instance MulHom.mulHomClass {M N : Type _} [Mul M] [Mul N] : MulHomClass (M →ₙ* N) M N where
  coe := MulHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
  map_mul := MulHom.map_mul'

def MulHomClass.toMulHom {M N F : Type _} [Mul M] [Mul N] [MulHomClass F M N] (f : F) : M →ₙ* N where
  toFun := f
  map_mul' := map_mul f

instance {M N F : Type _} [Mul M] [Mul N] [MulHomClass F M N] : CoeTC F (M →ₙ* N) :=
  ⟨MulHomClass.toMulHom⟩

structure AddMonoidHom (M : Type _) (N : Type _) [AddZeroClass M] [AddZeroClass N] extends
  ZeroHom M N, AddHom M N

infixr:25 " →+ " => AddMonoidHom

class AddMonoidHomClass (F : Type _) (M N : outParam (Type _)) [AddZeroClass M] [AddZeroClass N]
  extends AddHomClass F M N, ZeroHomClass F M N

instance AddMonoidHom.addMonoidHomClass {M : Type _} {N : Type _} [AddZeroClass M] [AddZeroClass N] : AddMonoidHomClass (M →+ N) M N where
  coe f := f.toFun
  coe_injective' f g h := sorry
  map_add := AddMonoidHom.map_add'
  map_zero f := f.toZeroHom.map_zero'

instance AddMonoidHom.coeToZeroHom [AddZeroClass M] [AddZeroClass N] :
  Coe (M →+ N) (ZeroHom M N) := ⟨AddMonoidHom.toZeroHom⟩

instance AddMonoidHom.coeToAddHom [AddZeroClass M] [AddZeroClass N] :
  Coe (M →+ N) (AddHom M N) := ⟨AddMonoidHom.toAddHom⟩

def AddMonoidHomClass.toAddMonoidHom {M N F : Type _} [AddZeroClass M] [AddZeroClass N] [AddMonoidHomClass F M N] (f : F) : M →+ N :=
  { (f : AddHom M N), (f : ZeroHom M N) with }

instance [AddZeroClass M] [AddZeroClass N] [AddMonoidHomClass F M N] : CoeTC F (M →+ N) :=
  ⟨AddMonoidHomClass.toAddMonoidHom⟩

structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

infixr:25 " →* " => MonoidHom

class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
  extends MulHomClass F M N, OneHomClass F M N

instance MonoidHom.monoidHomClass {M : Type _} {N : Type _} [MulOneClass M] [MulOneClass N] : MonoidHomClass (M →* N) M N where
  coe f := f.toFun
  coe_injective' f g h := sorry
  map_mul := MonoidHom.map_mul'
  map_one f := f.toOneHom.map_one'

instance MonoidHom.coeToOneHom [MulOneClass M] [MulOneClass N] :
  Coe (M →* N) (OneHom M N) := ⟨MonoidHom.toOneHom⟩

instance MonoidHom.coeToMulHom [MulOneClass M] [MulOneClass N] :
  Coe (M →* N) (M →ₙ* N) := ⟨MonoidHom.toMulHom⟩

def MonoidHomClass.toMonoidHom {M N F : Type _} [MulOneClass M] [MulOneClass N] [MonoidHomClass F M N] (f : F) : M →* N :=
  { (f : M →ₙ* N), (f : OneHom M N) with }

instance [MulOneClass M] [MulOneClass N] [MonoidHomClass F M N] : CoeTC F (M →* N) :=
  ⟨MonoidHomClass.toMonoidHom⟩

/-

## Rings 

-/

structure MonoidWithZeroHom (M : Type _) (N : Type _)
  [MulZeroOneClass M] [MulZeroOneClass N] extends ZeroHom M N, MonoidHom M N

/-- `M →*₀ N` denotes the type of zero-preserving monoid homomorphisms from `M` to `N`. -/
infixr:25 " →*₀ " => MonoidWithZeroHom
structure NonUnitalRingHom (α β : Type _) [NonUnitalNonAssocSemiring α]
  [NonUnitalNonAssocSemiring β] extends α →ₙ* β, α →+ β

class MonoidWithZeroHomClass (F : Type _) (M N : outParam (Type _)) [MulZeroOneClass M]
  [MulZeroOneClass N] extends MonoidHomClass F M N, ZeroHomClass F M N

instance MonoidWithZeroHom.monoidWithZeroHomClass {M : Type _} {N : Type _} [MulZeroOneClass M]
  [MulZeroOneClass N] : MonoidWithZeroHomClass (M →*₀ N) M N where
  coe f := f.toFun
  coe_injective' f g h := sorry
  map_mul := MonoidWithZeroHom.map_mul'
  map_one := MonoidWithZeroHom.map_one'
  map_zero f := f.map_zero'

-- def MonoidWithZeroHomClass.toMonoidWithZeroHom {M N F : Type _} [MulZeroOneClass M] [MulZeroOneClass N] 
--     [MonoidWithZeroHomClass F M N] (f : F) : M →*₀ N :=
--   { (f : M →* N), (f : ZeroHom M N) with }

-- /-- Any type satisfying `MonoidWithZeroHomClass` can be cast into `MonoidWithZeroHom` via
-- `MonoidWithZeroHomClass.toMonoidWithZeroHom`. -/
-- instance [MonoidWithZeroHomClass F M N] : CoeTC F (M →*₀ N) :=
--   ⟨MonoidWithZeroHomClass.toMonoidWithZeroHom⟩


/-- `MonoidWithZeroHom` down-cast to a `MonoidHom`, forgetting the 0-preserving property. -/
instance MonoidWithZeroHom.coeToMonoidHom [MulZeroOneClass M] [MulZeroOneClass N] :
  Coe (M →*₀ N) (M →* N) := ⟨MonoidWithZeroHom.toMonoidHom⟩

--attribute [coe] MonoidWithZeroHom.toZeroHom

/-- `MonoidWithZeroHom` down-cast to a `ZeroHom`, forgetting the monoidal property. -/
instance MonoidWithZeroHom.coeToZeroHom [MulZeroOneClass M] [MulZeroOneClass N] :
  Coe (M →*₀ N) (ZeroHom M N) := ⟨MonoidWithZeroHom.toZeroHom⟩

/-- `α →ₙ+* β` denotes the type of non-unital ring homomorphisms from `α` to `β`. -/
infixr:25 " →ₙ+* " => NonUnitalRingHom


structure RingHom (α : Type _) (β : Type _) [NonAssocSemiring α] [NonAssocSemiring β] extends
  α →* β, α →+ β, α →ₙ+* β, α →*₀ β

/-- `α →+* β` denotes the type of ring homomorphisms from `α` to `β`. -/
infixr:25 " →+* " => RingHom

class RingHomClass (F : Type _) (α β : outParam (Type _)) [NonAssocSemiring α]
  [NonAssocSemiring β] extends MonoidHomClass F α β, AddMonoidHomClass F α β,
  MonoidWithZeroHomClass F α β

def RingHomClass.toRingHom {F α β : Type _} {_ : NonAssocSemiring α}
  {_ : NonAssocSemiring β} [RingHomClass F α β] (f : F) : α →+* β :=
  { (f : α →* β), (f : α →+ β) with }

/-- Any type satisfying `RingHomClass` can be cast into `RingHom` via `RingHomClass.toRingHom`. -/
instance {F α β : Type _} {_ : NonAssocSemiring α}
  {_ : NonAssocSemiring β} [RingHomClass F α β] : CoeTC F (α →+* β) :=
  ⟨RingHomClass.toRingHom⟩

instance instRingHomClass {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} : RingHomClass (α →+* β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr
    apply FunLike.coe_injective'
    exact h
  map_add := RingHom.map_add'
  map_zero := RingHom.map_zero'
  map_mul f := f.map_mul'
  map_one f := f.map_one'

def RingHom.id (α : Type _) [NonAssocSemiring α] : α →+* α := by
  refine' { toFun := _root_.id.. } <;> intros <;> rfl

end RingHom



section Module

open Function

universe u v w

variable {α R k S M M₂ M₃ ι : Type _}

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a • b` computes the product of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hSMul : α → β → γ

class SMul (M : Type _) (α : Type _) where
  smul : M → α → α

infixr:73 " • " => HSMul.hSMul

instance instHSMul {α β : Type _} [SMul α β] : HSMul α β β where
  hSMul := SMul.smul

class MulAction (α : Type _) (β : Type _) [Monoid α] extends SMul α β where
  /-- One is the neutral element for `•` -/
  protected one_smul : ∀ b : β, (1 : α) • b = b
  /-- Associativity of `•` and `*` -/
  mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b

class DistribMulAction (M A : Type _) [Monoid M] [AddMonoid A] extends MulAction M A where
  /-- Multiplying `0` by a scalar gives `0` -/
  smul_zero : ∀ a : M, a • (0 : A) = 0
  /-- Scalar multiplication distributes across addition -/
  smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

--@[to_additive]
instance (priority := 910) Monoid.toMulAction (M : Type _) [Monoid M] :
    MulAction M M where
  smul := (· * ·)
  one_smul := one_mul
  mul_smul := sorry

class SMulZeroClass (M A : Type _) [Zero A] extends SMul M A where
  /-- Multiplying `0` by a scalar gives `0` -/
  smul_zero : ∀ a : M, a • (0 : A) = 0

/-- `SMulWithZero` is a class consisting of a Type `R` with `0 ∈ R` and a scalar multiplication
of `R` on a Type `M` with `0`, such that the equality `r • m = 0` holds if at least one among `r`
or `m` equals `0`. -/
class SMulWithZero (R M : Type _) [Zero R] [Zero M] extends SMulZeroClass R M where
  /-- Scalar multiplication by the scalar `0` is `0`. -/
  zero_smul : ∀ m : M, (0 : R) • m = 0

instance MulZeroClass.toSMulWithZero (R : Type _) [MulZeroClass R] : SMulWithZero R R where
  smul := (· * ·)
  smul_zero := mul_zero
  zero_smul := zero_mul

class MulActionWithZero (R : Type _) (M : Type _) [MonoidWithZero R] [Zero M] extends MulAction R M where
  smul_zero : ∀ r : R, r • (0 : M) = 0
  zero_smul : ∀ m : M, (0 : R) • m = 0

-- see Note [lower instance priority]
instance (priority := 100) MulActionWithZero.toSMulWithZero (R M : Type _) [MonoidWithZero R] [Zero M] 
    [m : MulActionWithZero R M] : SMulWithZero R M :=
  { m with }

/-- See also `Semiring.toModule` -/
instance MonoidWithZero.toMulActionWithZero (R : Type _) [MonoidWithZero R] : MulActionWithZero R R :=
  { MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }

class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends
  DistribMulAction R M where
  protected add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
  protected zero_smul : ∀ x : M, (0 : R) • x = 0

end Module

section AddCommMonoid

variable [Semiring R] [AddCommMonoid M] [Module R M] (r s : R) (x y : M)

-- see Note [lower instance priority]
/-- A module over a semiring automatically inherits a `MulActionWithZero` structure. -/
instance (priority := 100) Module.toMulActionWithZero : MulActionWithZero R M :=
  { (inferInstance : MulAction R M) with
    smul_zero := sorry
    zero_smul := sorry }

end AddCommMonoid

section Algebra

class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A,
  R →+* A where
  commutes' : ∀ r x, toRingHom r * x = x * toRingHom r
  smul_def' : ∀ r x, r • x = toRingHom r * x

--RingHom.toAlgebra

/-- Creating an algebra from a morphism to the center of a semiring. -/
def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
    (h : ∀ c x, i c * x = x * i c) : Algebra R S where
  smul c x := i c * x
  commutes' := h
  smul_def' _ _ := rfl
  toRingHom := i

/-- Creating an algebra from a morphism to a commutative semiring. -/
def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
  i.toAlgebra' fun _ => sorry

namespace Algebra

instance id {R : Type _} [CommSemiring R] : Algebra R R :=
  (RingHom.id R).toAlgebra

end Algebra

instance (priority := 910) Semiring.toModule [Semiring R] : Module R R where
  smul_add := sorry
  add_smul := sorry
  zero_smul := sorry
  smul_zero := sorry

end Algebra

namespace Pi

universe v w

variable {I : Type v}

variable {f : I → Type w}

instance instZero [∀ i, Zero <| f i] : Zero (∀ i : I, f i) :=
  ⟨fun _ => 0⟩

variable {M}

instance instSMul [∀ i, SMul M <| f i] : SMul M (∀ i : I, f i) :=
  ⟨fun s x => fun i => s • x i⟩

universe x

variable {α : Type x}

instance smulWithZero [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] :
    SMulWithZero α (∀ i, f i) :=
  { Pi.instSMul with
    -- already this is odd:
    -- smul_zero := fun a => funext fun i => SMulZeroClass.smul_zero a -- "failed to synthesize instance `SMulZeroClass α (f i)`"
    smul_zero := fun a => funext fun i => @SMulZeroClass.smul_zero  _ (f i) _ _ a -- needs the @
    zero_smul := fun _ => funext fun _ => SMulWithZero.zero_smul _ }

instance mulAction (α) {m : Monoid α} [∀ i, MulAction α <| f i] :
    @MulAction α (∀ i : I, f i) m where
  smul := (· • ·)
  mul_smul _ _ _ := funext fun _ => MulAction.mul_smul _ _ _
  one_smul _ := funext fun _ => MulAction.one_smul _

end Pi

section oliver_example

theorem Pi.smul_apply {I : Type} {f : I → Type} {β : Type} [∀ i, SMul β (f i)] (x : ∀ i, f i) (b : β) (i : I) : (b • x) i = b • (x i) :=
  rfl

instance (R : Type) [CommRing R] : CommSemiring R where
  mul_comm := CommRing.mul_comm

--set_option trace.Meta.isDefEq true in
example {α R : Type} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul -- comment out to make `simp` work without `_`
  simp only [Pi.smul_apply] -- fails with bar, succeeds with `Pi.smul_apply _`

end oliver_example