[Merged by Bors] - feat: port Algebra.BigOperators.Fin

[joneugster]

---

See Zulip question about to_additive.

• depends on: [Merged by Bors] - feat: port Data.Fintype.Fin #1847
• depends on: -- fix: fin bug in to_additive #1861 not really

[joneugster]

This theorem was a nightmare to prove. Lots of things that should be def-eq aren't recoginsed as such by rw (e.g. n + 1 vs n.succ). Moreover assoc_rw would be really helpful.

Could somebody look at the proof and decide if there is anything that could be done to avoid non-terminal simp and all the change?

[joneugster]

Also the statement has changed. In Lean3 it was ↑i instead of (Fin.castLt i (Nat.lt_succ_of_lt i.2)). I changed that because Lean4 got the conversion wrong, could that be fixed too?

[Vierkantor]

I see, Lean 4 coerces via the path Fin n → ℕ → Fin (n + 1) which results in different defeqs than castLt. Although I can't actually find where the coercion comes from in mathlib 3...

[Vierkantor]

Nope, turns out that Lean 3 finds the same coercion (@coe_trans (fin n) ℕ (fin (n + 1)) nat.cast_coe (fin.fin_to_nat n)). So I think it's best to keep the statement with a coercion.

[jcommelin]

Thanks for writing the extensive porting note.
Let's merge this PR now. We can revisit this issue later.

[jcommelin]

Thanks 🎉

bors merge

[bors]

👎 Rejected by label

[jcommelin]

bors r+

[semorrison]

This PR/issue depends on:

• [Merged by Bors] - feat: port Data.Fintype.Fin #1847
  By Dependent Issues (🤖). Happy coding!

[bors]

Build failed:

• Build

[jcommelin]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style