Data.List.BigOperators.Basic mathlib4#1380

Stream: mathlib4

[Johan Commelin]

I pushed a first pass on fixing some capitalization. But I need to do something else for a bit.

[Johan Commelin]

to_additive in

@[to_additive]
theorem prod_is_unit : ∀ {L : List M} (u : ∀ m ∈ L, IsUnit m), IsUnit L.prod
  | [], _ => by simp
  | h :: t, u => by
    simp only [List.prod_cons]
    exact IsUnit.mul (u h (mem_cons_self h t)) (prod_is_unit fun m mt => u m (mem_cons_of_mem h mt))
#align list.prod_is_unit List.prod_is_unit

errors with

application type mismatch
  Mathlib.Algebra.Group.Units._auxLemma.22
argument has type
  AddMonoid M
but function has type
  ∀ [inst : Monoid M], IsUnit 1 = True

[Johan Commelin]

Is to_additive forgetting to translate some stuff?

[Floris van Doorn]

This is mathlib4#1149, fixed by mathlib4#1314

[Johan Commelin]

Ok, good!

[Johan Commelin]

So we just need some people to review some meta PRs

[Scott Morrison]

I dealt with a few comments on mathlib4#1314.

[Johan Commelin]

5 out of 6 errors in this file have to do with to_additive.

[Johan Commelin]

So if we can get mathlib4#1314 in, that would be great.

[Johan Commelin]

My feeling is that it would also solve the final error.

[Johan Commelin]

This one seems back on track!

[Johan Commelin]

And CI is happy