-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x_1 : M
i : ι
h : Nontrivial R
x y : M
⊢ (fun (x : M) (i : ι) ↦
        ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
              (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
            (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                ((b : (a : ι) → M) i) ⋯ :
              { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
          R))
      (x + y) =
    HAdd.hAdd (α := ι → R)
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        x)
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        y)
have h : ∀ (i : ι),
  (fun (x : M) (i : ι) ↦
        ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
              (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
            (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                ((b : (a : ι) → M) i) sorry :
              { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
          R))
      (x + y) i =
    HAdd.hAdd (α := ι → R) (β := ι → R)
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) sorry :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        x)
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) sorry :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        y)
      i
Tactic: ext i