awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
g₁ : relations₁.G
r₂ : relations₂.R
inr :
  Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦
            solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2 :
          (a : relations₁.G × relations₂.G →₀ A) → M₁ ⊗[A] M₂)
        (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A fun (x : (relations₁.tensor relations₂).G) ↦
            match (motive := (relations₁.tensor relations₂).G → M₁ ⊗[A] M₂) x with
            | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂ :
          (a : (relations₁.tensor relations₂).G →₀ A) → M₁ ⊗[A] M₂)
        ((relations₁.tensor relations₂).relation (Sum.inr (g₁, r₂))) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
g₁ : relations₁.G
r₂ : relations₂.R
inr :
  Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A
            ((fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦ solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2) ∘
              (⇑(Function.Embedding.sectR g₁ relations₂.G) : (a : relations₂.G) → relations₁.G × relations₂.G)) :
          (a : relations₂.G →₀ A) → M₁ ⊗[A] M₂)
        (relations₂.relation r₂) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦
            solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2 :
          (a : relations₁.G × relations₂.G →₀ A) → M₁ ⊗[A] M₂)
        (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)

Tactic:
rw [Finsupp.linearCombination_embDomain]

Premises used: Finsupp.linearCombination_embDomain
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
g₁ : relations₁.G
r₂ : relations₂.R
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A
            ((fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦ solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2) ∘
              (⇑(Function.Embedding.sectR g₁ relations₂.G) : (a : relations₂.G) → relations₁.G × relations₂.G)) :
          (a : relations₂.G →₀ A) → M₁ ⊗[A] M₂)
        (relations₂.relation r₂) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)

Tactic:
(solution₂.postcomp (curry .id (solution₁.var g₁))).linearCombination_var_relation r₂

Premises used: LinearMap.id, TensorProduct.tmul, TensorProduct.curry, Module.Relations.Solution.postcomp, DFunLike.coe, AddCon.toQuotient, Module.Relations.Solution.linearCombination_var_relation, Module.Relations.Solution.var
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
g₁ : relations₁.G
r₂ : relations₂.R
⊢ Eq (α := M₁ ⊗[A] M₂)
    ((Finsupp.linearCombination A
            ((fun (x : Prod.{w₁₀, w₂₀} relations₁.G relations₂.G) ↦ solution₁.var x.1 ⊗ₜ[A] solution₂.var x.2) ∘
              (⇑(Function.Embedding.sectR g₁ relations₂.G) : (a : relations₂.G) → relations₁.G × relations₂.G)) :
          (a : relations₂.G →₀ A) → M₁ ⊗[A] M₂)
        (relations₂.relation r₂) :
      M₁ ⊗[A] M₂)
    (0 : M₁ ⊗[A] M₂)

Tactic:
exact (solution₂.postcomp (curry .id (solution₁.var g₁))).linearCombination_var_relation r₂

Premises used: LinearMap.id, TensorProduct.curry, Module.Relations.Solution.postcomp, DFunLike.coe, Module.Relations.Solution.linearCombination_var_relation, Module.Relations.Solution.var
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
g₁ : relations₁.G
r₂ : relations₂.R
erw :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : relations₁.G × relations₂.G →₀ A) → N)
        (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
      N)
    (0 : N)
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂) : (a : relations₂.G →₀ A) → N)
        (relations₂.relation r₂) :
      N)
    (0 : N)

Tactic:
erw [← Finsupp.linearCombination_embDomain A
              (Function.Embedding.sectR g₁ relations₂.G)]

Premises used: Finsupp.linearCombination_embDomain, Module.Relations.G, Function.Embedding.sectR
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
g₁ : relations₁.G
r₂ : relations₂.R
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : relations₁.G × relations₂.G →₀ A) → N)
        (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
      N)
    (0 : N)

Tactic:
s.linearCombination_var_relation (.inr ⟨g₁, r₂⟩)

Premises used: Set.Mem, setOf, Prod.mk, Sum.inr, Finsupp.embDomain, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
g₁ : relations₁.G
r₂ : relations₂.R
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : relations₁.G × relations₂.G →₀ A) → N)
        (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) :
      N)
    (0 : N)

Tactic:
exact s.linearCombination_var_relation (.inr ⟨g₁, r₂⟩)

Premises used: Prod.mk, Sum.inr, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
var :
  ∀ (g₂ : relations₂.G),
    Eq.{w + 1} (α := N)
      (Solution.var
        (solution₂.postcomp
          ((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
                h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
              (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
            (relations₁.relation r₁)))
        g₂)
      (Solution.var (solution₂.postcomp 0) g₂)
⊢ Eq (α := relations₂.Solution N)
    (solution₂.postcomp
      ((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
            h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
          (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
        (relations₁.relation r₁)))
    (solution₂.postcomp 0)

Tactic:
ext g₂
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
var :
  Eq.{w + 1} (α := N)
    ((((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
                  h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
                (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
              (relations₁.relation r₁) :
            M₂ →ₗ[A] N) :
          (a : M₂) → N)
        (solution₂.var g₂) :
      N)
    (0 : N)
⊢ Eq.{w + 1} (α := N)
    (Solution.var
      (solution₂.postcomp
        ((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
            (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
          (relations₁.relation r₁)))
      g₂)
    (Solution.var (solution₂.postcomp 0) g₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
var :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (Function.comp (β := M₂ →ₗ[A] N)
              (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
                (a : M₂ →ₗ[A] N) → N)
              fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
⊢ Eq.{w + 1} (α := N)
    ((((Finsupp.linearCombination A fun (g₁ : relations₁.G) ↦
                  h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ } :
                (a : relations₁.G →₀ A) → M₂ →ₗ[A] N)
              (relations₁.relation r₁) :
            M₂ →ₗ[A] N) :
          (a : M₂) → N)
        (solution₂.var g₂) :
      N)
    (0 : N)

Tactic:
erw [Finsupp.apply_linearCombination A (LinearMap.applyₗ (solution₂.var g₂))]

Premises used: LinearMap.applyₗ, Finsupp.apply_linearCombination, DFunLike.coe, Module.Relations.Solution.var
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : (relations₁.tensor relations₂).G →₀ A) → N)
        ((relations₁.tensor relations₂).relation (Sum.inl (r₁, g₂))) :
      N)
    (0 : N)

Tactic:
have := s.linearCombination_var_relation (.inl ⟨r₁, g₂⟩)
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : (relations₁.tensor relations₂).G →₀ A) → N)
        ((relations₁.tensor relations₂).relation (Sum.inl (r₁, g₂))) :
      N)
    (0 : N)
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)

Tactic:
erw [Finsupp.linearCombination_embDomain] at this

Premises used: Finsupp.linearCombination_embDomain
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)

Tactic:
this
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
h :
  Eq (α := relations₁.G → N)
    (Function.comp (β := M₂ →ₗ[A] N)
      (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
        (a : M₂ →ₗ[A] N) → N)
      fun (g₁ : relations₁.G) ↦
      h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
    (s.var ∘ (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G))
⊢ Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (Function.comp (β := M₂ →ₗ[A] N)
              (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
                (a : M₂ →ₗ[A] N) → N)
              fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)

Tactic:
convert! this
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
h :
  ∀ (g₁ : relations₁.G),
    Function.comp (β := M₂ →ₗ[A] N)
        (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
          (a : M₂ →ₗ[A] N) → N)
        (fun (g₁ : relations₁.G) ↦
          h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
        g₁ =
      (s.var ∘ (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) g₁
⊢ Eq (α := relations₁.G → N)
    (Function.comp (β := M₂ →ₗ[A] N)
      (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
        (a : M₂ →ₗ[A] N) → N)
      fun (g₁ : relations₁.G) ↦
      h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
    (s.var ∘ (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G))

Tactic:
ext g₁
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
s : (relations₁.tensor relations₂).Solution N
r₁ : relations₁.R
g₂ : relations₂.G
this :
  Eq.{w + 1} (α := N)
    ((Finsupp.linearCombination A
            (s.var ∘
              (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) :
          (a : relations₁.G →₀ A) → N)
        (relations₁.relation r₁) :
      N)
    (0 : N)
g₁ : relations₁.G
⊢ Function.comp (β := M₂ →ₗ[A] N)
      (⇑((LinearMap.applyₗ : (a : M₂) → (M₂ →ₗ[A] N) →ₗ[A] N) (solution₂.var g₂) : (M₂ →ₗ[A] N) →ₗ[A] N) :
        (a : M₂ →ₗ[A] N) → N)
      (fun (g₁ : relations₁.G) ↦
        h₂.desc { var := fun (g₂ : relations₂.G) ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
      g₁ =
    (s.var ∘ (⇑(Function.Embedding.sectL relations₁.G g₂) : (a : relations₁.G) → (relations₁.tensor relations₂).G)) g₁

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
x : (relations₁.tensor relations₂).Solution N
⊢ (solution₁.tensor solution₂).postcomp
      ((uncurry (RingHom.id A) M₁ M₂ N : (a : M₁ →ₗ[A] M₂ →ₗ[A] N) → M₁ ⊗[A] M₂ →ₗ[A] N)
        (h₁.desc
          {
            var := fun (g₁ : relations₁.G) ↦
              h₂.desc { var := fun (g₂ : relations₂.G) ↦ x.var (g₁, g₂), linearCombination_var_relation := ⋯ },
            linearCombination_var_relation := ⋯ })) =
    x

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
f f' : M₁ ⊗[A] M₂ →ₗ[A] N
h : (solution₁.tensor solution₂).postcomp f = (solution₁.tensor solution₂).postcomp f'
var :
  ∀ (g₁ : relations₁.G),
    Eq (α := M₂ →ₗ[A] N)
      (Solution.var
        (solution₁.postcomp
          (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
        g₁)
      (Solution.var
        (solution₁.postcomp
          (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
        g₁)
⊢ Eq (α := relations₁.Solution (M₂ →ₗ[A] N))
    (solution₁.postcomp
      (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
    (solution₁.postcomp
      (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))

Tactic:
ext g₁ : 2
-- Module: Mathlib.Algebra.Module.Presentation.Tensor
Goal:
A : Type u
inst : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
relations₁ : Relations.{w₁₀, w₁₁, u} A
relations₂ : Relations.{w₂₀, w₂₁, u} A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N : Type w
inst_5 : AddCommGroup N
inst_6 : Module A N
f f' : M₁ ⊗[A] M₂ →ₗ[A] N
h : (solution₁.tensor solution₂).postcomp f = (solution₁.tensor solution₂).postcomp f'
g₁ : relations₁.G
⊢ Eq (α := M₂ →ₗ[A] N)
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f))
      g₁)
    (var
      (solution₁.postcomp
        (curry.{u, u, v₁, v₂, w} (R := A) (R₂ := A) (σ₁₂ := RingHom.id A) (M := M₁) (N := M₂) (P₂ := N) f'))
      g₁)

Tactic:
h₂.postcomp_injective ?_

Premises used: Module.Relations.Solution.IsPresentation.postcomp_injective