awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Module.Finite R M
rw : Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
rw₁ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton M
rw₂ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton.{u_2 + 1} (Submodule R M)
rw₃ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊤
rw₄ :
  Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔
    Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (R := R) (M := M) (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1)
        ⊥)
      ⊤
rw₅ rw₆ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M

Tactic:
rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]

Premises used: Submodule.subsingleton_iff, Submodule.map_bot, IsLocalRing.map_tensorProduct_mk_eq_top, subsingleton_iff_bot_eq_top
-- 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 : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), Eq (α := k ⊗[R] M) (1 ⊗ₜ[R] f i) ((b : (a : ι) → k ⊗[R] M) i)
rw :
  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) ∘ f)))
    (Submodule.span k (Set.range (ι := ι) (⇑b : (a : ι) → k ⊗[R] M)))
⊢ Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤

Tactic:
rw [← map_tensorProduct_mk_eq_top, Submodule.map_span, ← Submodule.restrictScalars_span R k
    Ideal.Quotient.mk_surjective, Submodule.restrictScalars_eq_top_iff,
    ← b.span_eq, ← Set.range_comp]

Premises used: Set.range_comp, IsLocalRing.map_tensorProduct_mk_eq_top, Submodule.map_span, Submodule.restrictScalars_eq_top_iff, Module.Basis.span_eq
-- 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 : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), Eq (α := k ⊗[R] M) (1 ⊗ₜ[R] f i) ((b : (a : ι) → k ⊗[R] M) i)
⊢ 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) ∘ f)))
    (Submodule.span k (Set.range (ι := ι) (⇑b : (a : ι) → k ⊗[R] M)))

Tactic:
simp only [Function.comp_def, mk_apply, hb, Basis.span_eq]

Premises used: TensorProduct.mk_apply, Function.comp_def, Module.Basis.span_eq
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₁ :
  Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₂ :
  Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₃ :
  ¬Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₄ :
  Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₅ :
  Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Subsingleton (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₆ rw₇ :
  Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Subsingleton (Localization.AtPrime p.asIdeal ⊗[R] M)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)

Tactic:
rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]

Premises used: not_iff_not, Equiv.nontrivial_congr, not_nontrivial_iff_subsingleton, LinearEquiv.toAddEquiv, LocalizedModule.equivTensorProduct, Module.mem_support_iff, Ideal.primeCompl, IsLocalRing.subsingleton_tensorProduct, AddEquiv.toEquiv, PrimeSpectrum.asIdeal
-- 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₂)
rw :
  ∀ (a : M₃ ⊗[R] N₁),
    Eq (α := M₃ ⊗[R] N₂) ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂) a : M₃ ⊗[R] N₂) (0 : M₃ ⊗[R] N₂) →
      a = 0
⊢ Function.Injective (α := M₃ ⊗[R] N₁) (β := M₃ ⊗[R] N₂) (⇑(LinearMap.lTensor M₃ g₁) : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- 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₂) x : M₃ ⊗[R] N₂) (0 : M₃ ⊗[R] N₂)
obtain :
  ∀ (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₁)
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := f₂.rTensor_surjective N₁ hfsurj x

Premises used: LinearMap.rTensor_surjective, 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₂)
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₂)
rw₄ 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₂)
⊢ 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:
rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]

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₂)
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₂)
        ((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]
-- 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₂)
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₁)
⊢ 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

Premises used: rTensor_exact, Iff.mp
-- 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₂)
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₃)
⊢ Eq (α := M₁ ⊗[R] N₃) ((LinearMap.lTensor M₁ g₂ : (a : M₁ ⊗[R] N₂) → M₁ ⊗[R] N₃) y : M₁ ⊗[R] N₃) (0 : M₁ ⊗[R] N₃)

Tactic:
apply hfinj
-- 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₂)
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₃)
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₃)
⊢ 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:
trans g₂.lTensor M₂ (g₁.lTensor M₂ x)

Premises used: LinearMap.lTensor, DFunLike.coe
-- 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₂)
rw :
  Eq (α := M₂ ⊗[R] N₃) ((LinearMap.lTensor M₂ 0 : (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₃)
⊢ 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:
rw [← LinearMap.comp_apply, ← LinearMap.lTensor_comp, hgexact.linearMap_comp_eq_zero]

Premises used: LinearMap.comp_apply, Function.Exact.linearMap_comp_eq_zero, LinearMap.lTensor_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₂)
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₂ 0 : (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:
simp