Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) 0) =
    (LinearMap.rTensor M (of R ι G f x✝²)) 0

pp: case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ ∀ (x : G x✝²) (y : M),
    (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) (x ⊗ₜ[R] y)) =
      (LinearMap.rTensor M (of R ι G f x✝²)) (x ⊗ₜ[R] y)

pp: case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ ∀ (x y : G x✝² ⊗[R] M),
    (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) x) =
        (LinearMap.rTensor M (of R ι G f x✝²)) x →
      (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) y) =
          (LinearMap.rTensor M (of R ι G f x✝²)) y →
        (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) (x + y)) =
          (LinearMap.rTensor M (of R ι G f x✝²)) (x + y)

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) 0) =
    (LinearMap.rTensor M (of R ι G f x✝²)) 0

case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ ∀ (x : G x✝²) (y : M),
    (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) (x ⊗ₜ[R] y)) =
      (LinearMap.rTensor M (of R ι G f x✝²)) (x ⊗ₜ[R] y)

case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ ∀ (x y : G x✝² ⊗[R] M),
    (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) x) =
        (LinearMap.rTensor M (of R ι G f x✝²)) x →
      (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) y) =
          (LinearMap.rTensor M (of R ι G f x✝²)) y →
        (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) (x + y)) =
          (LinearMap.rTensor M (of R ι G f x✝²)) (x + y)