awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
solution : relations.Solution M
h₁ : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
assumption
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
s : M₂ → Finsupp.{w₂₀, u} pres₂.G A
hs : ∀ (m₂ : M₂), (pres₂.π : (a : pres₂.G →₀ A) → M₂) (s m₂) = m₂
i : ι
⊢ Eq.{v₂ + 1} (α := M₂) ((pres₂.π : (a : pres₂.G →₀ A) → M₂) (s ((f : (a : M₁) → M₂) (g₁ i))) : M₂)
    ((f : (a : M₁) → M₂) (g₁ i) : M₂)

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
obtain :
  ∀ (s : M₂ → Finsupp.{w₂₀, u} pres₂.G A) (hs : Function.RightInverse s (⇑pres₂.π : (a : pres₂.G →₀ A) → M₂)),
    Nonempty (pres₂.CokernelData f g₁)
⊢ Nonempty (pres₂.CokernelData f g₁)

Tactic:
obtain ⟨s, hs⟩ := pres₂.surjective_π.hasRightInverse

Premises used: Function.Surjective.hasRightInverse, Module.Presentation.toIsPresentation, Module.Relations.Solution.IsPresentation.surjective_π
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
s : M₂ → Finsupp.{w₂₀, u} pres₂.G A
hs : Function.RightInverse s (⇑pres₂.π : (a : pres₂.G →₀ A) → M₂)
⊢ Nonempty (pres₂.CokernelData f g₁)

Tactic:
⟨CokernelData.ofSection _ _ _ s hs⟩

Premises used: Nonempty.intro, Module.Presentation.CokernelData.ofSection
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
s : M₂ → Finsupp.{w₂₀, u} pres₂.G A
hs : Function.RightInverse s (⇑pres₂.π : (a : pres₂.G →₀ A) → M₂)
⊢ Nonempty (pres₂.CokernelData f g₁)

Tactic:
exact ⟨CokernelData.ofSection _ _ _ s hs⟩
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
x : (pres₂.cokernelRelations data).R
erw :
  Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation x)) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
⊢ Eq.{v₂ + 1} (α := M₂ ⧸ f.range)
    ((Finsupp.linearCombination A fun (g : (pres₂.cokernelRelations data).G) ↦
            (f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) (pres₂.var g) :
          (a : (pres₂.cokernelRelations data).G →₀ A) → M₂ ⧸ f.range)
        ((pres₂.cokernelRelations data).relation x) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)

Tactic:
erw [← Finsupp.apply_linearCombination]

Premises used: Finsupp.apply_linearCombination
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
x : (pres₂.cokernelRelations data).R
inl :
  ∀ (r : pres₂.R),
    Eq (α := M₂ ⧸ f.range)
      ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
          ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
            ((pres₂.cokernelRelations data).relation (Sum.inl r))) :
        M₂ ⧸ f.range)
      (0 : M₂ ⧸ f.range)
inr :
  ∀ (i : ι),
    Eq (α := M₂ ⧸ f.range)
      ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
          ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
            ((pres₂.cokernelRelations data).relation (Sum.inr i))) :
        M₂ ⧸ f.range)
      (0 : M₂ ⧸ f.range)
⊢ Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation x)) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)

Tactic:
obtain (r | i) := x
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
r : pres₂.R
inl : Eq (α := M₂ ⧸ f.range) ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) 0) 0
⊢ Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation (Sum.inl r))) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)

Tactic:
erw [pres₂.linearCombination_var_relation]

Premises used: Module.Presentation.toSolution, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
r : pres₂.R
⊢ Eq (α := M₂ ⧸ f.range) ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) 0) 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
i : ι
inr :
  Eq (α := M₂ ⧸ f.range) ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) ((f : (a : M₁) → M₂) (g₁ i)) : M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)
⊢ Eq (α := M₂ ⧸ f.range)
    ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range)
        ((Finsupp.linearCombination A pres₂.var : (a : (pres₂.cokernelRelations data).G →₀ A) → M₂)
          ((pres₂.cokernelRelations data).relation (Sum.inr i))) :
      M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)

Tactic:
erw [data.π_lift]

Premises used: Module.Presentation.CokernelData.π_lift
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
i : ι
⊢ Eq (α := M₂ ⧸ f.range) ((f.range.mkQ : (a : M₂) → M₂ ⧸ f.range) ((f : (a : M₁) → M₂) (g₁ i)) : M₂ ⧸ f.range)
    (0 : M₂ ⧸ f.range)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
s : (pres₂.cokernelRelations data).Solution N
rw :
  Set.range g₁ ⊆
    (⇑f : (a : M₁) → M₂) ⁻¹'
      (↑(LinearMap.ker.{u, u, v₂, w} (M₂ := N)
            (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ : pres₂.Solution N })) :
        Set M₂)
⊢ f.range ≤ LinearMap.ker.{u, u, v₂, w} (M₂ := N) (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ })

Tactic:
rw [LinearMap.range_eq_map, ← hg₁, Submodule.map_span, Submodule.span_le,
            Set.image_subset_iff]

Premises used: LinearMap.range_eq_map, Set.image_subset_iff, Submodule.map_span, Submodule.span_le
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
s : (pres₂.cokernelRelations data).Solution N
i : ι
rw :
  Eq.{w + 1} (α := N)
    ((Relations.Solution.π { var := s.var, linearCombination_var_relation := ⋯ } : (a : pres₂.G →₀ A) → N)
        (data.lift i) :
      N)
    (0 : N)
⊢ Membership.mem (γ := Set M₁)
    ((⇑f : (a : M₁) → M₂) ⁻¹'
      (↑(LinearMap.ker.{u, u, v₂, w} (M₂ := N)
            (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ : pres₂.Solution N })) :
        Set M₂))
    (g₁ i)

Tactic:
rw [Set.mem_preimage, SetLike.mem_coe, LinearMap.mem_ker, ← data.π_lift,
            Relations.Solution.IsPresentation.π_desc_apply]

Premises used: Module.Presentation.CokernelData.π_lift, LinearMap.mem_ker, SetLike.mem_coe, Set.mem_preimage, Module.Relations.Solution.IsPresentation.π_desc_apply
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
s : (pres₂.cokernelRelations data).Solution N
i : ι
⊢ Eq.{w + 1} (α := N)
    ((Relations.Solution.π { var := s.var, linearCombination_var_relation := ⋯ } : (a : pres₂.G →₀ A) → N)
        (data.lift i) :
      N)
    (0 : N)

Tactic:
s.linearCombination_var_relation (.inr i)

Premises used: Sum.inr, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
s : (pres₂.cokernelRelations data).Solution N
i : ι
⊢ Eq.{w + 1} (α := N)
    ((Relations.Solution.π { var := s.var, linearCombination_var_relation := ⋯ } : (a : pres₂.G →₀ A) → N)
        (data.lift i) :
      N)
    (0 : N)

Tactic:
exact s.linearCombination_var_relation (.inr i)

Premises used: Sum.inr, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
s : (pres₂.cokernelRelations data).Solution N
⊢ (pres₂.cokernelSolution data).postcomp
      (f.range.liftQ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ : pres₂.Solution N }) ⋯) =
    s

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
h₁ : f_1 ∘ₗ f.range.mkQ = f' ∘ₗ f.range.mkQ
⊢ f_1 = f'

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
h₁ : pres₂.postcomp (f_1 ∘ₗ f.range.mkQ) = pres₂.postcomp (f' ∘ₗ f.range.mkQ)
⊢ f_1 ∘ₗ f.range.mkQ = f' ∘ₗ f.range.mkQ

Tactic:
apply pres₂.toIsPresentation.postcomp_injective

Premises used: Module.Presentation.toIsPresentation, Module.Relations.Solution.IsPresentation.postcomp_injective
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
h₁ : ∀ (g : pres₂.G), (pres₂.postcomp (f_1 ∘ₗ f.range.mkQ)).var g = (pres₂.postcomp (f' ∘ₗ f.range.mkQ)).var g
⊢ pres₂.postcomp (f_1 ∘ₗ f.range.mkQ) = pres₂.postcomp (f' ∘ₗ f.range.mkQ)

Tactic:
ext g
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
g : pres₂.G
⊢ (pres₂.postcomp (f_1 ∘ₗ f.range.mkQ)).var g = (pres₂.postcomp (f' ∘ₗ f.range.mkQ)).var g

Tactic:
Relations.Solution.congr_var h g

Premises used: Module.Relations.Solution.congr_var
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
inst_5 : AddCommGroup M₃
inst_6 : Module A M₃
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
N : Type w
inst_7 : AddCommGroup N
inst_8 : Module A N
f_1 f' : LinearMap.{u, u, v₂, w} (RingHom.id A) (M₂ ⧸ f.range) N
h : (pres₂.cokernelSolution data).postcomp f_1 = (pres₂.cokernelSolution data).postcomp f'
g : pres₂.G
⊢ (pres₂.postcomp (f_1 ∘ₗ f.range.mkQ)).var g = (pres₂.postcomp (f' ∘ₗ f.range.mkQ)).var g

Tactic:
exact Relations.Solution.congr_var h g

Premises used: Module.Relations.Solution.congr_var
-- Module: Mathlib.Algebra.Module.Presentation.Cokernel
Goal:
A : Type u
inst : Ring A
M₁ : Type v₁
M₂ : Type v₂
inst_1 : AddCommGroup M₁
inst_2 : Module A M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₂
pres₂ : Presentation.{w₂₀, w₂₁, v₂, u} A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Eq (α := Submodule A M₁) (Submodule.span A (Set.range g₁)) ⊤
⊢ (pres₂.cokernelSolution data).IsPresentation

Tactic:
(isPresentationCore pres₂ data hg₁).isPresentation

Premises used: Module.Relations.Solution.IsPresentationCore.isPresentation, Module.Presentation.cokernelSolution.isPresentationCore
-- 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.{v + 1} (α := S) ((algebraMap pres.Ring S : (a : pres.Ring) → S) 0 : S) (0 : S)

Tactic:
simp
-- 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 :
  ∀ (a : ι),
    Eq (α := Ω[S⁄R])
      (((pres.toExtension.toKaehler ∘ₗ
              (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace)) ∘ₗ
            Finsupp.lsingle a :
          (a : S) → Ω[S⁄R])
        1)
      (((Finsupp.linearCombination S fun (g : ι) ↦ (D R S : (a : S) → Ω[S⁄R]) (pres.val g)) ∘ₗ Finsupp.lsingle a :
          (a : S) → Ω[S⁄R])
        1)
⊢ pres.toExtension.toKaehler ∘ₗ (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace) =
    Finsupp.linearCombination S fun (g : ι) ↦ (D R S : (a : S) → Ω[S⁄R]) (pres.val g)

Tactic:
ext
-- 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 ι σ
a : ι
⊢ Eq (α := Ω[S⁄R])
    (((pres.toExtension.toKaehler ∘ₗ
            (↑pres.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] pres.toExtension.CotangentSpace)) ∘ₗ
          Finsupp.lsingle a :
        (a : S) → Ω[S⁄R])
      1)
    (((Finsupp.linearCombination S fun (g : ι) ↦ (D R S : (a : S) → Ω[S⁄R]) (pres.val g)) ∘ₗ Finsupp.lsingle a :
        (a : S) → Ω[S⁄R])
      1)

Tactic:
simp
-- 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.relation r ∈ pres.toExtension.ker

Tactic:
simp
-- 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.Cotangent)
    ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1) : pres.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : pres.toExtension.Ring) ↦ x ∈ pres.toExtension.ker) (pres.relation r) ⋯) :
      pres.toExtension.Cotangent)

Tactic:
simp [hom₁]

Premises used: Algebra.Presentation.differentials.hom₁
-- 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 ι σ
⊢ ∀ (x y : σ →₀ S),
    (hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (x + y) =
      HAdd.hAdd (α := pres.toExtension.Cotangent) (β := pres.toExtension.Cotangent)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) x : pres.toExtension.Cotangent)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) y : pres.toExtension.Cotangent)

Tactic:
simp
-- 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 ι σ
⊢ ∀ (m : pres.Ring) (x : σ →₀ S),
    (hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) (m • x) =
      HSMul.hSMul (α := pres.Ring) (β := pres.toExtension.Cotangent)
        ((RingHom.id pres.Ring : (a : pres.Ring) → pres.Ring) m : pres.Ring)
        ((hom₁ pres : (a : σ →₀ S) → pres.toExtension.Cotangent) x : pres.toExtension.Cotangent)

Tactic:
simp
-- 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 ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
change :
  Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent) (⇑φ : (a : σ →₀ S) → pres.toExtension.Cotangent)
⊢ Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent)
    (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent)

Tactic:
change Function.Surjective φ

Premises used: DFunLike.coe, Function.Surjective
-- 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 ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
⊢ Function.Surjective (α := ↥pres.toExtension.ker) (β := pres.toExtension.Cotangent)
    (⇑Extension.Cotangent.mk : (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)

Tactic:
have h₁ := Algebra.Extension.Cotangent.mk_surjective (P := pres.toExtension)
-- 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 ι σ
φ : LinearMap (R := pres.Ring) (RingHom.id pres.Ring) (σ →₀ S) pres.toExtension.Cotangent :=
  { toFun := (⇑(hom₁ pres) : (a : σ →₀ S) → pres.toExtension.Cotangent), map_add' := ⋯, map_smul' := ⋯ }
h₁ :
  Function.Surjective (α := ↥pres.toExtension.ker) (β := pres.toExtension.Cotangent)
    (⇑Extension.Cotangent.mk : (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
r : σ
⊢ pres.relation r ∈ pres.ker

Tactic:
simp