-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst_6 : (i : ι) → Fintype (κ₁ i)
inst_7 : ∀ (i : ι), Finite.{u_8 + 1} (κ₂ i)
inst_8 : (i : ι) → DecidableEq (κ₁ i)
inst_9 : Fintype ι
b₁ : (i : ι) → Basis.{u_7, u_4, u_5} (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis.{u_8, u_4, u_6} (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo (⇑f : (a : M₁) → M₂) (↑(N₁ i) : Set M₁) (↑(N₂ i) : Set M₂)
i : ι
snd : κ₂ i
j : ι
snd_1 : κ₁ j
a :
  ∀ (snd_2 : κ₁ i),
    Eq.{u_4 + 1} (α := R)
      (((((h₂.collectedBasis (α := κ₂) b₂).repr : (a : M₂) → (i : ι) × κ₂ i →₀ R)
                ((f : (a : M₁) → M₂)
                  ((h₁.collectedBasis (α := κ₁) b₁ : (a : (i : ι) × κ₁ i) → M₁)
                      (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) i snd_2) :
                    M₁)) :
              (i : ι) × κ₂ i →₀ R) :
            (a : (i : ι) × κ₂ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) :
        R)
      (if h : i = i then
          ((((b₂ i).repr : (a : ↥(N₂ i)) → κ₂ i →₀ R)
                  (((f.restrict ⋯ : LinearMap.{u_4, u_4, u_5, u_6} (RingHom.id R) ↥(N₁ i) ↥(N₂ i)) :
                      (a : ↥(N₁ i)) → ↥(N₂ i))
                    ((b₁ i : (a : κ₁ i) → ↥(N₁ i)) (cast ⋯ snd_2))) :
                Finsupp.{u_8, u_4} (κ₂ i) R) :
              (a : κ₂ i) → R)
            snd
        else 0 :
        R)
⊢ Eq.{u_4 + 1} (α := R)
    (((((h₂.collectedBasis (α := κ₂) b₂).repr : (a : M₂) → (i : ι) × κ₂ i →₀ R)
              ((f : (a : M₁) → M₂)
                ((h₁.collectedBasis (α := κ₁) b₁ : (a : (i : ι) × κ₁ i) → M₁)
                    (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
                  M₁)) :
            (i : ι) × κ₂ i →₀ R) :
          (a : (i : ι) × κ₂ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) :
      R)
    (if h : i = j then
        ((((b₂ i).repr : (a : ↥(N₂ i)) → κ₂ i →₀ R)
                (((f.restrict ⋯ : LinearMap.{u_4, u_4, u_5, u_6} (RingHom.id R) ↥(N₁ i) ↥(N₂ i)) :
                    (a : ↥(N₁ i)) → ↥(N₂ i))
                  ((b₁ i : (a : κ₁ i) → ↥(N₁ i)) (cast ⋯ snd_1))) :
              Finsupp.{u_8, u_4} (κ₂ i) R) :
            (a : κ₂ i) → R)
          snd
      else 0 :
      R)
have a₁ : ∀ (hij : i ≠ j),
  Eq.{u_4 + 1} (α := R)
    (((((h₂.collectedBasis (α := κ₂) b₂).repr : (a : M₂) → (i : ι) × κ₂ i →₀ R)
              ((f : (a : M₁) → M₂)
                ((h₁.collectedBasis (α := κ₁) b₁ : (a : (i : ι) × κ₁ i) → M₁)
                    (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
                  M₁)) :
            (i : ι) × κ₂ i →₀ R) :
          (a : (i : ι) × κ₂ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) :
      R)
    (if h : i = j then
        ((((b₂ i).repr : (a : ↥(N₂ i)) → κ₂ i →₀ R)
                (((f.restrict sorry : LinearMap.{u_4, u_4, u_5, u_6} (RingHom.id R) ↥(N₁ i) ↥(N₂ i)) :
                    (a : ↥(N₁ i)) → ↥(N₂ i))
                  ((b₁ i : (a : κ₁ i) → ↥(N₁ i)) (cast sorry snd_1))) :
              Finsupp.{u_8, u_4} (κ₂ i) R) :
            (a : κ₂ i) → R)
          snd
      else 0 :
      R)
Tactic: rcases eq_or_ne i j with rfl | hij