unable to import Mathlib.Algebra.BigOperators

Stream: mathlib4

[Eric]

I try to build a toy project to prove 1+...+n=n(n+1)/2, migrating an answer using Mathlib3: https://stackoverflow.com/questions/59595896/how-to-prove-mathematical-induction-formulae-in-lean-theorem-prover.

import Mathlib.Algebra.BigOperators
import Mathlib.Tactic.Ring

open Finset

example (n : ℕ) : 2 * (range (n + 1)).sum id = n * (n + 1) := by
  induction n with
  | zero =>
    -- Base case: n = 0
    rw [range_zero, sum_empty]
    simp
  | succ n ih =>
    -- Inductive step: assume true for n, prove for n + 1
    rw [sum_range_succ, mul_add, ih, id.def, Nat.succ_eq_add_one]
    ring

But I got an error

`<toolchain_path>/bin/lake setup-file <project_path>/Test.lean Init Mathlib.Algebra.BigOperators Mathlib.Tactic.Ring --no-build --no-cache` failed:

stderr:
✖ [2/632] Running Mathlib.Algebra.BigOperators
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Algebra/BigOperators.lean
✖ [630/632] Running imports (<project_path>/Test.lean)
error: <project_path>/Test.lean: bad import 'Mathlib.Algebra.BigOperators'
Some required builds logged failures:
- Mathlib.Algebra.BigOperators
- imports (<project_path>/Test.lean)
error: build failed

Why am I unable to import Mathlib.Algebra.BigOperators? How to fix this?

[Vlad Tsyrklevich]

There is no Mathlib/Algebra/BigOperators.lean, Mathlib/Algebra/BigOperators/ is a directory so you need to import a specific file under that directory. If you're just developing locally, you can use import Mathlib at the top to import everything.

[Vlad Tsyrklevich]

in this case, the specific import you want is Mathlib.Algebra.BigOperators.Group.Finset, which I found by looking up the documentation for Finset.sum_range_succ