awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
⊢ Eq (α := pres.toExtension.CotangentSpace)
    (1 ⊗ₜ[pres.toExtension.Ring]
        (D R pres.toExtension.Ring : (a : pres.toExtension.Ring) → Ω[pres.toExtension.Ring⁄R]) (pres.relation r) :
      TensorProduct pres.toExtension.Ring S Ω[pres.toExtension.Ring⁄R])
    ((Finsupp.linearCombination S (⇑pres.cotangentSpaceBasis : (a : ι) → pres.toExtension.CotangentSpace) :
          (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        (Finsupp.mapRange (⇑(algebraMap pres.Ring S) : (a : pres.Ring) → S) ⋯
          ((Basis.repr (mvPolynomialBasis R ι) : (a : Ω[MvPolynomial ι R⁄R]) → ι →₀ MvPolynomial ι R)
            ((D R (MvPolynomial ι R) : (a : MvPolynomial ι R) → Ω[MvPolynomial ι R⁄R]) (pres.relation r)))) :
      pres.toExtension.CotangentSpace)

Tactic:
exact pres.cotangentSpaceBasis.repr.injective (by ext; simp)

Premises used: Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, LinearEquiv.injective, Algebra.Presentation.toGenerators
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
h :
  ∀ (r : σ),
    Eq (α := pres.toExtension.CotangentSpace)
      (((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r :
          (a : S) → pres.toExtension.CotangentSpace)
        1)
      ((((↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) ∘ₗ
              pres.differentialsRelations.map) ∘ₗ
            Finsupp.lsingle r :
          (a : S) → pres.toExtension.CotangentSpace)
        1)
⊢ pres.toExtension.cotangentComplex ∘ₗ hom₁ pres =
    (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) ∘ₗ
      pres.differentialsRelations.map

Tactic:
ext r
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
⊢ ∀ (r : pres.differentialsRelations.R),
    (pres.differentialsRelations.map : (a : pres.differentialsRelations.R →₀ S) → pres.differentialsRelations.G →₀ S)
        (Finsupp.single r 1) =
      pres.differentialsRelations.relation r

Tactic:
have := (differentialsRelations pres).map_single
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
this :
  ∀ (r : pres.differentialsRelations.R),
    (pres.differentialsRelations.map : (a : pres.differentialsRelations.R →₀ S) → pres.differentialsRelations.G →₀ S)
        (Finsupp.single r 1) =
      pres.differentialsRelations.relation r
h :
  Eq (α := pres.toExtension.CotangentSpace)
    ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
⊢ Eq (α := pres.toExtension.CotangentSpace)
    (((pres.toExtension.cotangentComplex ∘ₗ hom₁ pres) ∘ₗ Finsupp.lsingle r : (a : S) → pres.toExtension.CotangentSpace)
      1)
    ((((↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) ∘ₗ
            pres.differentialsRelations.map) ∘ₗ
          Finsupp.lsingle r :
        (a : S) → pres.toExtension.CotangentSpace)
      1)

Tactic:
dsimp at this ⊢
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : σ
this :
  ∀ (r : σ),
    (pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1) =
      pres.differentialsRelations.relation r
h :
  Eq (α := pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        (pres.differentialsRelations.relation r) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
h₁ h₂ :
  Eq (α := pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        (pres.differentialsRelations.relation r) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        (pres.differentialsRelations.relation r) :
      pres.toExtension.CotangentSpace)
⊢ Eq (α := pres.toExtension.CotangentSpace)
    ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)
    ((pres.cotangentSpaceBasis.repr.symm : (a : ι →₀ S) → pres.toExtension.CotangentSpace)
        ((pres.differentialsRelations.map : (a : σ →₀ S) → ι →₀ S) (Finsupp.single r 1)) :
      pres.toExtension.CotangentSpace)

Tactic:
rw [comm₁₂_single, this]

Premises used: Algebra.Presentation.differentials.comm₁₂_single
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : pres.differentialsRelations.R
simp :
  Eq.{v + 1} (α := Ω[S⁄R])
    ((pres.toExtension.toKaehler : (a : pres.toExtension.CotangentSpace) → Ω[S⁄R])
        ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
          ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1))) :
      Ω[S⁄R])
    (0 : Ω[S⁄R])
⊢ Eq.{v + 1} (α := Ω[S⁄R])
    ((Finsupp.linearCombination S fun (g : pres.differentialsRelations.G) ↦ (D R S : (a : S) → Ω[S⁄R]) (pres.val g) :
          (a : pres.differentialsRelations.G →₀ S) → Ω[S⁄R])
        (pres.differentialsRelations.relation r) :
      Ω[S⁄R])
    (0 : Ω[S⁄R])

Tactic:
simp only [differentialsRelations_G, LinearMap.coe_comp, LinearEquiv.coe_coe,
      Function.comp_apply, ← comm₂₃', ← comm₁₂_single]

Premises used: Algebra.Presentation.differentials.comm₁₂_single, Algebra.Presentation.differentials.comm₂₃', LinearMap.coe_comp, Function.comp_apply, Algebra.Presentation.differentialsRelations_G, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
r : pres.differentialsRelations.R
⊢ Eq.{v + 1} (α := Ω[S⁄R])
    ((pres.toExtension.toKaehler : (a : pres.toExtension.CotangentSpace) → Ω[S⁄R])
        ((pres.toExtension.cotangentComplex : (a : pres.toExtension.Cotangent) → pres.toExtension.CotangentSpace)
          ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1))) :
      Ω[S⁄R])
    (0 : Ω[S⁄R])

Tactic:
apply DFunLike.congr_fun (Function.Exact.linearMap_comp_eq_zero
      (pres.toExtension.exact_cotangentComplex_toKaehler))

Premises used: DFunLike.congr_fun, Function.Exact.linearMap_comp_eq_zero, Algebra.Extension.exact_cotangentComplex_toKaehler
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ pres.toExtension.toKaehler ∘ₗ (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) =
    pres.differentialsSolution.π

Tactic:
comm₂₃' pres

Premises used: Algebra.Presentation.differentials.comm₂₃', Module.Relations.Solution.π
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
left : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤
right : pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤ ∧
    pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
left :
  Function.Surjective (α := Finsupp.{w, v} pres.differentialsRelations.G S) (β := Ω[S⁄R])
    (⇑(pres.toExtension.toKaehler ∘ₗ
          (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace)) :
      (a : pres.differentialsRelations.G →₀ S) → Ω[S⁄R])
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range pres.differentialsSolution.var)) ⊤

Tactic:
rw [← Module.Relations.Solution.surjective_π_iff_span_eq_top, ← comm₂₃]

Premises used: Module.Relations.Solution.surjective_π_iff_span_eq_top, Algebra.Presentation.differentials.comm₂₃
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ Function.Surjective (α := Finsupp.{w, v} pres.differentialsRelations.G S) (β := Ω[S⁄R])
    (⇑(pres.toExtension.toKaehler ∘ₗ
          (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace)) :
      (a : pres.differentialsRelations.G →₀ S) → Ω[S⁄R])

Tactic:
Extension.toKaehler_surjective.comp pres.cotangentSpaceBasis.repr.symm.surjective

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.surjective, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, Algebra.Extension.toKaehler_surjective, Function.Surjective.comp, Algebra.Presentation.toGenerators
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ Function.Surjective (α := Finsupp.{w, v} pres.differentialsRelations.G S) (β := Ω[S⁄R])
    (⇑(pres.toExtension.toKaehler ∘ₗ
          (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace)) :
      (a : pres.differentialsRelations.G →₀ S) → Ω[S⁄R])

Tactic:
exact Extension.toKaehler_surjective.comp pres.cotangentSpaceBasis.repr.symm.surjective

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, Algebra.Extension.toKaehler_surjective, Function.Surjective.comp, Algebra.Presentation.toGenerators
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
right : pres.differentialsSolution.π.ker = pres.differentialsRelations.map.range
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
rw [← Module.Relations.range_map]

Premises used: Module.Relations.range_map
-- Module: Mathlib.Algebra.Module.Presentation.Differentials
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = pres.differentialsRelations.map.range

Tactic:
exact Function.Exact.linearMap_ker_eq
      ((LinearMap.exact_iff_of_surjective_of_bijective_of_injective
      _ _ _ _ (hom₁ pres)
      pres.cotangentSpaceBasis.repr.symm.toLinearMap .id
      (comm₁₂ pres) (by simpa using comm₂₃ pres) (surjective_hom₁ pres)
        (LinearEquiv.bijective _) (Equiv.refl _).injective).2
        pres.toExtension.exact_cotangentComplex_toKaehler)
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
rw :
  Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (g : (relations i).G) ↦
            s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
          (a : (relations i).G →₀ A) → N)
        ((relations i).relation r) :
      N)
    ((Finsupp.linearCombination A s.var : (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (g : (relations i).G) ↦
            s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
          (a : (relations i).G →₀ A) → N)
        ((relations i).relation r) :
      N)
    (0 : N)

Tactic:
rw [← s.linearCombination_var_relation ⟨i, r⟩]

Premises used: Sigma.mk, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
symm :
  Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
    ((Finsupp.linearCombination A fun (g : (relations i).G) ↦
            s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
          (a : (relations i).G →₀ A) → N)
        ((relations i).relation r) :
      N)
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (g : (relations i).G) ↦
            s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
          (a : (relations i).G →₀ A) → N)
        ((relations i).relation r) :
      N)
    ((Finsupp.linearCombination A s.var : (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)

Tactic:
symm
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A s.var : (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
    ((Finsupp.linearCombination A fun (g : (relations i).G) ↦
            s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
          (a : (relations i).G →₀ A) → N)
        ((relations i).relation r) :
      N)

Tactic:
apply Finsupp.linearCombination_embDomain

Premises used: Finsupp.linearCombination_embDomain
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
t : (i : ι) → (relations i).Solution N
x : (directSum relations).R
i : ι
r : (relations i).R
rw :
  Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (x : (directSum relations).G) ↦
            match (motive := (directSum relations).G → N) x with
            | ⟨i, g⟩ => (t i).var g :
          (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
    ((Finsupp.linearCombination A (t i).var : (a : (relations i).G →₀ A) → N) ((relations i).relation r) : N)
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (x : (directSum relations).G) ↦
            match (motive := (directSum relations).G → N) x with
            | ⟨i, g⟩ => (t i).var g :
          (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
    (0 : N)

Tactic:
rw [← (t i).linearCombination_var_relation r]

Premises used: Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
t : (i : ι) → (relations i).Solution N
x : (directSum relations).R
i : ι
r : (relations i).R
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (x : (directSum relations).G) ↦
            match (motive := (directSum relations).G → N) x with
            | ⟨i, g⟩ => (t i).var g :
          (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
    ((Finsupp.linearCombination A (t i).var : (a : (relations i).G →₀ A) → N) ((relations i).relation r) : N)

Tactic:
apply Finsupp.linearCombination_embDomain

Premises used: Finsupp.linearCombination_embDomain
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
i : ι
g : (relations i).G
⊢ (directSum (M := M) solution).var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) =
    (lof A ι M i : (a : M i) → ⨁ (i : ι), M i) ((solution i).var g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N_1 : Type w'
inst_6 : AddCommGroup N_1
inst_7 : Module A N_1
s : (Relations.directSum relations).Solution N_1
var :
  ∀ (i : ι) (g : (relations i).G),
    Solution.var
        ((directSum (M := M) solution).postcomp
          (toModule A ι (M := M) N_1 fun (i : ι) ↦
            ⋯.desc
              ((directSumEquiv :
                  (a : (Relations.directSum relations).Solution N_1) → (i : ι) → (relations i).Solution N_1)
                s i)))
        (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) =
      s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g)
⊢ (directSum (M := M) solution).postcomp
      (toModule A ι (M := M) N_1 fun (i : ι) ↦
        ⋯.desc
          ((directSumEquiv : (a : (Relations.directSum relations).Solution N_1) → (i : ι) → (relations i).Solution N_1)
            s i)) =
    s

Tactic:
ext ⟨i, g⟩
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N_1 : Type w'
inst_6 : AddCommGroup N_1
inst_7 : Module A N_1
s : (Relations.directSum relations).Solution N_1
i : ι
g : (relations i).G
⊢ var
      ((directSum (M := M) solution).postcomp
        (toModule A ι (M := M) N_1 fun (i : ι) ↦
          ⋯.desc
            ((directSumEquiv :
                (a : (Relations.directSum relations).Solution N_1) → (i : ι) → (relations i).Solution N_1)
              s i)))
      (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) =
    s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N_1 : Type w'
inst_6 : AddCommGroup N_1
inst_7 : Module A N_1
f f' : (⨁ (i : ι), M i) →ₗ[A] N_1
h' : (directSum (M := M) solution).postcomp f = (directSum (M := M) solution).postcomp f'
H : ∀ (i : ι), f ∘ₗ lof A ι M i = f' ∘ₗ lof A ι M i
⊢ f = f'

Tactic:
ext i : 1
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N_1 : Type w'
inst_6 : AddCommGroup N_1
inst_7 : Module A N_1
f f' : (⨁ (i : ι), M i) →ₗ[A] N_1
h' : (directSum (M := M) solution).postcomp f = (directSum (M := M) solution).postcomp f'
i : ι
H : (solution i).postcomp (f ∘ₗ lof A ι M i) = (solution i).postcomp (f' ∘ₗ lof A ι M i)
⊢ f ∘ₗ lof A ι M i = f' ∘ₗ lof A ι M i

Tactic:
apply (h i).postcomp_injective

Premises used: Module.Relations.Solution.IsPresentation.postcomp_injective
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N_1 : Type w'
inst_6 : AddCommGroup N_1
inst_7 : Module A N_1
f f' : (⨁ (i : ι), M i) →ₗ[A] N_1
h' : (directSum (M := M) solution).postcomp f = (directSum (M := M) solution).postcomp f'
i : ι
H :
  ∀ (g : (relations i).G),
    ((solution i).postcomp (f ∘ₗ lof A ι M i)).var g = ((solution i).postcomp (f' ∘ₗ lof A ι M i)).var g
⊢ (solution i).postcomp (f ∘ₗ lof A ι M i) = (solution i).postcomp (f' ∘ₗ lof A ι M i)

Tactic:
ext g
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N_1 : Type w'
inst_6 : AddCommGroup N_1
inst_7 : Module A N_1
f f' : (⨁ (i : ι), M i) →ₗ[A] N_1
h' : (directSum (M := M) solution).postcomp f = (directSum (M := M) solution).postcomp f'
i : ι
g : (relations i).G
⊢ ((solution i).postcomp (f ∘ₗ lof A ι M i)).var g = ((solution i).postcomp (f' ∘ₗ lof A ι M i)).var g

Tactic:
Solution.congr_var h' ⟨i, g⟩

Premises used: Sigma.mk, Module.Relations.Solution.congr_var