awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Module
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₃)

Tactic:
have : g₂.lTensor M₁ y = 0 := by
    apply hfinj
    trans g₂.lTensor M₂ (g₁.lTensor M₂ x)
    · rw [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
        LinearMap.lTensor_comp_rTensor]
    rw [← LinearMap.comp_apply, ← LinearMap.lTensor_comp, hgexact.linearMap_comp_eq_zero]
    simp
-- Module: Mathlib.RingTheory.LocalRing.Module
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_1 :
  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₂)
this : Eq (α := M₁ ⊗[R] N₃) ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y : M₁ ⊗[R] N₃) (0 : M₁ ⊗[R] N₃)
obtain :
  ∀ (z : M₁ ⊗[R] N₁)
    (hy :
      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₂) z) :
          M₂ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂))
    (this :
      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₂) z) :
          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₁)
⊢ 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 ⟨z, rfl⟩ := (lTensor_exact _ hgexact hgsurj _).mp this

Premises used: lTensor_exact, Iff.mp, rfl
-- Module: Mathlib.RingTheory.LocalRing.Module
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_1 :
  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₂)
z : M₁ ⊗[R] N₁
hy :
  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₂) z) :
      M₂ ⊗[R] N₂)
    ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)
this :
  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₂) z) :
      M₁ ⊗[R] N₃)
    (0 : M₁ ⊗[R] N₃)
a :
  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₁) z) :
      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₁) z = x

Tactic:
apply hginj
-- Module: Mathlib.RingTheory.LocalRing.Module
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_1 :
  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₂)
z : M₁ ⊗[R] N₁
hy :
  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₂) z) :
      M₂ ⊗[R] N₂)
    ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)
this :
  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₂) z) :
      M₁ ⊗[R] N₃)
    (0 : M₁ ⊗[R] N₃)
⊢ 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₁) z) :
      M₂ ⊗[R] N₂)
    ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x : M₂ ⊗[R] N₂)

Tactic:
simp only [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.lTensor_comp_rTensor,
      LinearMap.rTensor_comp_lTensor]

Premises used: LinearMap.rTensor_comp_lTensor, LinearMap.comp_apply, LinearMap.lTensor_comp_rTensor
-- Module: Mathlib.RingTheory.LocalRing.Module
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₂)
z : M₁ ⊗[R] N₁
this_1 :
  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₂) z) :
      M₁ ⊗[R] N₃)
    (0 : 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₁)
          ((LinearMap.rTensor N₁ f₁ : (a : M₁ ⊗[R] N₁) → M₂ ⊗[R] N₁) z)) :
      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₂)
          ((LinearMap.rTensor N₁ f₁ : (a : M₁ ⊗[R] N₁) → M₂ ⊗[R] N₁) z)) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
hy :
  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₂) z) :
      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₁) z) :
      M₂ ⊗[R] N₂)
rw : Eq (α := M₃ ⊗[R] N₁) ((LinearMap.rTensor N₁ 0 : (a : M₁ ⊗[R] N₁) → M₃ ⊗[R] N₁) z : M₃ ⊗[R] N₁) (0 : M₃ ⊗[R] N₁)
⊢ Eq (α := M₃ ⊗[R] N₁)
    ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁)
        ((LinearMap.rTensor N₁ f₁ : (a : M₁ ⊗[R] N₁) → M₂ ⊗[R] N₁) z) :
      M₃ ⊗[R] N₁)
    (0 : M₃ ⊗[R] N₁)

Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.rTensor_comp, hfexact.linearMap_comp_eq_zero]

Premises used: LinearMap.comp_apply, Function.Exact.linearMap_comp_eq_zero, LinearMap.rTensor_comp
-- Module: Mathlib.RingTheory.LocalRing.Module
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₂)
z : M₁ ⊗[R] N₁
this_1 :
  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₂) z) :
      M₁ ⊗[R] N₃)
    (0 : 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₁)
          ((LinearMap.rTensor N₁ f₁ : (a : M₁ ⊗[R] N₁) → M₂ ⊗[R] N₁) z)) :
      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₂)
          ((LinearMap.rTensor N₁ f₁ : (a : M₁ ⊗[R] N₁) → M₂ ⊗[R] N₁) z)) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
hy :
  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₂) z) :
      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₁) z) :
      M₂ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₁) ((LinearMap.rTensor N₁ 0 : (a : M₁ ⊗[R] N₁) → M₃ ⊗[R] N₁) z : M₃ ⊗[R] N₁) (0 : M₃ ⊗[R] N₁)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
rw rw₁ : LE.le (α := Submodule k (k ⊗[R] M)) ⊤ ⊤
⊢ LE.le (α := Submodule k (k ⊗[R] M)) ⊤
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))

Tactic:
rw [hsp]
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
⊢ Finite ι

Tactic:
haveI : Finite ι := Module.Finite.finite_basis bk
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
rw : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
⊢ Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)

Tactic:
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
x : ι
⊢ Eq (α := k ⊗[R] M) (1 ⊗ₜ[R] v x) ((bk : (a : ι) → k ⊗[R] M) x)

Tactic:
simp [bk]
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
⊢ Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤

Tactic:
refine IsLocalRing.span_eq_top_of_tmul_eq_basis (R := R) (f := v) bk
      (fun _ ↦ by simp [bk])

Premises used: IsLocalRing.span_eq_top_of_tmul_eq_basis
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
⊢ Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)

Tactic:
have hi : Surjective i := by
    rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]
    refine IsLocalRing.span_eq_top_of_tmul_eq_basis (R := R) (f := v) bk
      (fun _ ↦ by simp [bk])
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
⊢ Module.Finite R ↥i.ker

Tactic:
have : Module.Finite R (LinearMap.ker i) :=
    .of_fg (Module.FinitePresentation.fg_ker i hi)
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
refine : Function.Injective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
⊢ (ι →₀ R) ≃ₗ[R] M

Tactic:
refine LinearEquiv.ofBijective i ⟨?_, hi⟩

Premises used: And.intro, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
rw : ∀ (y : k ⊗[R] ↥i.ker), y = 0
⊢ Function.Injective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)

Tactic:
rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
      ← IsLocalRing.subsingleton_tensorProduct (R := R), subsingleton_iff_forall_eq 0]

Premises used: Submodule.subsingleton_iff_eq_bot, LinearMap.ker_eq_bot, subsingleton_iff_forall_eq, IsLocalRing.subsingleton_tensorProduct, OfNat.ofNat