awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
rw :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
have rw₁ : Eq (α := M₃ ⊗[R] N₂)
  ((LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
  ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
      ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
    M₃ ⊗[R] N₂)
Tactic: rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
rw :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
rw₁ :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
have rw₂ : Eq (α := M₃ ⊗[R] N₂)
  ((LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
  ((LinearMap.lTensor M₃ g₁ ∘ₗ LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
Tactic: rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
rw :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
rw₁ :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
rw₂ :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ ∘ₗ LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
have rw₃ : Eq (α := M₃ ⊗[R] N₂) ((map f₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
  ((LinearMap.lTensor M₃ g₁ ∘ₗ LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
Tactic: rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
rw :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
rw₁ :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
rw₂ :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ ∘ₗ LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
rw₃ :
  Eq (α := M₃ ⊗[R] N₂) ((map f₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ ∘ₗ LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
have rw₄ : Eq (α := M₃ ⊗[R] N₂) ((map f₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
  ((map f₂ g₁ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂)
Tactic: rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₁) ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x : M₃ ⊗[R] N₁) (0 : M₃ ⊗[R] N₁)
have this : Eq (α := M₃ ⊗[R] N₂)
  ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
      ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
    M₃ ⊗[R] N₂)
  (0 : M₃ ⊗[R] N₂)
Tactic: have : f₂.rTensor N₂ (g₁.lTensor M₂ x) = 0 := by
    rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
this :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₁) ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x : M₃ ⊗[R] N₁) (0 : M₃ ⊗[R] N₁)
have obtain : ∀ (y : M₁ ⊗[R] N₂)
  (hy :
    Eq (α := M₂ ⊗[R] N₂) ((LinearMap.rTensor N₂ f₁ : (a : M₁ ⊗[R] N₂) → M₂ ⊗[R] N₂) y : M₂ ⊗[R] N₂)
      ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)),
  Eq (α := M₃ ⊗[R] N₁) ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x : M₃ ⊗[R] N₁) (0 : M₃ ⊗[R] N₁)
Tactic: obtain ⟨y, hy⟩ := (rTensor_exact N₂ hfexact hfsurj _).mp this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
this :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
y : M₁ ⊗[R] N₂
hy :
  Eq (α := M₂ ⊗[R] N₂) ((LinearMap.rTensor N₂ f₁ : (a : M₁ ⊗[R] N₂) → M₂ ⊗[R] N₂) y : M₂ ⊗[R] N₂)
    ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)
⊢ Eq (α := M₁ ⊗[R] N₃) ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y : M₁ ⊗[R] N₃) (0 : M₁ ⊗[R] N₃)
have a : Eq (α := M₂ ⊗[R] N₃)
  ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
      ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y) :
    M₂ ⊗[R] N₃)
  ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃) 0 : M₂ ⊗[R] N₃)
Tactic: apply hfinj
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
this :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
y : M₁ ⊗[R] N₂
hy :
  Eq (α := M₂ ⊗[R] N₂) ((LinearMap.rTensor N₂ f₁ : (a : M₁ ⊗[R] N₂) → M₂ ⊗[R] N₂) y : M₂ ⊗[R] N₂)
    ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)
⊢ Eq (α := M₂ ⊗[R] N₃)
    ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
        ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y) :
      M₂ ⊗[R] N₃)
    ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃) 0 : M₂ ⊗[R] N₃)
have trans : Eq (α := M₂ ⊗[R] N₃)
  ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
      ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y) :
    M₂ ⊗[R] N₃)
  ((LinearMap.lTensor M₂ g₂ : (a : M₂ ⊗[R] N₂) → M₂ ⊗[R] N₃)
      ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
    M₂ ⊗[R] N₃)
Tactic: trans g₂.lTensor M₂ (g₁.lTensor M₂ x)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
this :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
y : M₁ ⊗[R] N₂
hy :
  Eq (α := M₂ ⊗[R] N₂) ((LinearMap.rTensor N₂ f₁ : (a : M₁ ⊗[R] N₂) → M₂ ⊗[R] N₂) y : M₂ ⊗[R] N₂)
    ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)
trans :
  Eq (α := M₂ ⊗[R] N₃)
    ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
        ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y) :
      M₂ ⊗[R] N₃)
    ((LinearMap.lTensor M₂ g₂ : (a : M₂ ⊗[R] N₂) → M₂ ⊗[R] N₃)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₂ ⊗[R] N₃)
⊢ Eq (α := M₂ ⊗[R] N₃)
    ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
        ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y) :
      M₂ ⊗[R] N₃)
    ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃) 0 : M₂ ⊗[R] N₃)
have trans₁ : Eq (α := M₂ ⊗[R] N₃)
  ((LinearMap.lTensor M₂ g₂ : (a : M₂ ⊗[R] N₂) → M₂ ⊗[R] N₃)
      ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
    M₂ ⊗[R] N₃)
  ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃) 0 : M₂ ⊗[R] N₃)
Tactic: trans g₂.lTensor M₂ (g₁.lTensor M₂ x)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
this :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
y : M₁ ⊗[R] N₂
hy :
  Eq (α := M₂ ⊗[R] N₂) ((LinearMap.rTensor N₂ f₁ : (a : M₁ ⊗[R] N₂) → M₂ ⊗[R] N₂) y : M₂ ⊗[R] N₂)
    ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)
⊢ Eq (α := M₂ ⊗[R] N₃)
    ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
        ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y) :
      M₂ ⊗[R] N₃)
    ((LinearMap.lTensor M₂ g₂ : (a : M₂ ⊗[R] N₂) → M₂ ⊗[R] N₃)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₂ ⊗[R] N₃)
have rw : Eq (α := M₂ ⊗[R] N₃)
  ((LinearMap.rTensor N₃ f₁ : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
      ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y) :
    M₂ ⊗[R] N₃)
  ((LinearMap.lTensor M₂ g₂ : (a : M₂ ⊗[R] N₂) → M₂ ⊗[R] N₃)
      ((LinearMap.rTensor N₂ f₁ : (a : M₁ ⊗[R] N₂) → M₂ ⊗[R] N₂) y) :
    M₂ ⊗[R] N₃)
Tactic: rw [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
        LinearMap.lTensor_comp_rTensor]