-- 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
x_1 x_2 : ι
h : x_1 ≤ x_2
x : TensorProduct.{u_1, u_3, u_4} R (G x_1) M
refine_1 :
  Eq (α := Module.DirectLimit G f ⊗[R] M)
    (((fun (x : ι) ↦
            (LinearMap.rTensor M (of R ι G f x) :
              TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
          x_2 :
        (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
      ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) 0))
    (((fun (x : ι) ↦
            (LinearMap.rTensor M (of R ι G f x) :
              TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
          x_1 :
        (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
      0)
refine_2 :
  ∀ (x : G x_1) (y : M),
    Eq (α := Module.DirectLimit G f ⊗[R] M)
      (((fun (x : ι) ↦
                (LinearMap.rTensor M (of R ι G f x) :
                  TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
              x_2 :
            (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
          ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) (x ⊗ₜ[R] y)) :
        Module.DirectLimit G f ⊗[R] M)
      (((fun (x : ι) ↦
                (LinearMap.rTensor M (of R ι G f x) :
                  TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
              x_1 :
            (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
          (x ⊗ₜ[R] y) :
        Module.DirectLimit G f ⊗[R] M)
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M)
    (((fun (x : ι) ↦
              (LinearMap.rTensor M (of R ι G f x) :
                TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
            x_2 :
          (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
        ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) x) :
      Module.DirectLimit G f ⊗[R] M)
    (((fun (x : ι) ↦
              (LinearMap.rTensor M (of R ι G f x) :
                TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
            x_1 :
          (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
        x :
      Module.DirectLimit G f ⊗[R] M)
have refine_3 : ∀ (x y : TensorProduct.{u_1, u_3, u_4} R (G x_1) M),
  Eq (α := Module.DirectLimit G f ⊗[R] M)
      (((fun (x : ι) ↦
                (LinearMap.rTensor M (of R ι G f x) :
                  TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
              x_2 :
            (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
          ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) x) :
        Module.DirectLimit G f ⊗[R] M)
      (((fun (x : ι) ↦
                (LinearMap.rTensor M (of R ι G f x) :
                  TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
              x_1 :
            (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
          x :
        Module.DirectLimit G f ⊗[R] M) →
    Eq (α := Module.DirectLimit G f ⊗[R] M)
        (((fun (x : ι) ↦
                  (LinearMap.rTensor M (of R ι G f x) :
                    TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                x_2 :
              (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
            ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) y) :
          Module.DirectLimit G f ⊗[R] M)
        (((fun (x : ι) ↦
                  (LinearMap.rTensor M (of R ι G f x) :
                    TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                x_1 :
              (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
            y :
          Module.DirectLimit G f ⊗[R] M) →
      Eq (α := Module.DirectLimit G f ⊗[R] M)
        (((fun (x : ι) ↦
                  (LinearMap.rTensor M (of R ι G f x) :
                    TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                x_2 :
              (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
            ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) (x + y)) :
          Module.DirectLimit G f ⊗[R] M)
        (((fun (x : ι) ↦
                  (LinearMap.rTensor M (of R ι G f x) :
                    TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
                x_1 :
              (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
            (x + y) :
          Module.DirectLimit G f ⊗[R] M)
Tactic: refine x.induction_on ?_ ?_ ?_