-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.DirectLimit (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
i : ι
g : G i
m : M
⊢ Eq (α :=
    Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
      LinearMap.rTensor M (f i j h))
    ((toDirectLimit (G := G) f M :
          (a : Module.DirectLimit G f ⊗[R] M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        ((of R ι G f i : (a : G i) → Module.DirectLimit G f) g ⊗ₜ[R] m) :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
    (((of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
              (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) i :
            TensorProduct.{u_1, u_3, u_4} R (G i) M →ₗ[R]
              Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
          (a : G i ⊗[R] M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        (g ⊗ₜ[R] m) :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
have rw : Eq (α :=
  Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
    LinearMap.rTensor M (f i j h))
  ((((LinearMap.compr₂ (mk R (G i) M)
                (of R ι (fun (_i : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G _i) M)
                  (fun (_i _j : ι) (h : _i ≤ _j) ↦ LinearMap.rTensor M (f _i _j h)) i) :
              (a : G i) →
                M →ₗ[R]
                  Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦
                    LinearMap.rTensor M (f i j h))
            g :
          M →ₗ[R]
            Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
              fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
        (a : M) →
          Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
      m :
    Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
      LinearMap.rTensor M (f i j h))
  (((of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
            (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) i :
          TensorProduct.{u_1, u_3, u_4} R (G i) M →ₗ[R]
            Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
              fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
        (a : G i ⊗[R] M) →
          Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
      (g ⊗ₜ[R] m) :
    Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
      LinearMap.rTensor M (f i j h))
Tactic: rw [toDirectLimit, lift.tmul, lift_of]