-- 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 : M
i : ι
h : Nontrivial R
apply :
  ∀ (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)
apply₁ :
  ∀ (c : R) (x : 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))
        (c • x) =
      HSMul.hSMul (β := ι → R) c
        ((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)
⊢ Eq.{u_11 + 1} (α := R)
    ((((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)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
have apply₂ : ∀ (i : ι),
  Eq (α := ι → 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))
      ((b : (a : ι) → M) i))
    (⇑(single i 1) : (a : ι) → R)
Tactic: apply (b.repr_apply_eq (fun x i => b.reindexRange.repr x ⟨b i, _⟩) _ _ _ x i).symm