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 ι σ
φ : 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)
⊢ Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤

Tactic:
Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker)
      Subtype.coe_injective ?_

Premises used: Set.Mem, Subtype.coe_injective, Submodule.map_injective_of_injective
-- 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)
refine :
  Submodule.map (Submodule.subtype pres.ker)
      (Submodule.span pres.Ring
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) =
    Submodule.map (Submodule.subtype pres.ker) ⊤
⊢ Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤

Tactic:
refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker)
      Subtype.coe_injective ?_

Premises used: Subtype.coe_injective, Submodule.map_injective_of_injective
-- 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)
rw :
  Ideal.span
      (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) =
    pres.ker
⊢ Submodule.map (Submodule.subtype pres.ker)
      (Submodule.span pres.Ring
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) =
    Submodule.map (Submodule.subtype pres.ker) ⊤

Tactic:
rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span,
      Submodule.coe_subtype, Ideal.submodule_span_eq]

Premises used: Ideal.submodule_span_eq, Submodule.map_top, Submodule.coe_subtype, Submodule.map_span, Submodule.range_subtype
-- 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)
simp :
  Eq (α := Submodule pres.Ring pres.Ring)
    (Ideal.span
      (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)))
    (Ideal.span (Set.range pres.relation))
⊢ Ideal.span
      (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) =
    pres.ker

Tactic:
simp only [← pres.span_range_relation_eq_ker]

Premises used: Algebra.Presentation.span_range_relation_eq_ker
-- 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)
e_s :
  Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) =
    Set.range pres.relation
⊢ Eq (α := Submodule pres.Ring pres.Ring)
    (Ideal.span
      (Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)))
    (Ideal.span (Set.range pres.relation))

Tactic:
congr
-- 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)
⊢ Set.image (α := ↥pres.ker) (Subtype.val (p := fun (x : pres.Ring) ↦ x ∈ pres.ker))
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) =
    Set.range pres.relation

Tactic:
aesop
-- 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)
⊢ Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤

Tactic:
have h₂ : Submodule.span pres.Ring
      (Set.range (fun r ↦ (⟨pres.relation r, by simp⟩ : pres.ker))) = ⊤ := by
    refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker)
      Subtype.coe_injective ?_
    rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span,
      Submodule.coe_subtype, Ideal.submodule_span_eq]
    simp only [← pres.span_range_relation_eq_ker]
    congr
    aesop
-- 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)
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
rw :
  ∀
    (h₁ :
      Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤)
    (h₂ :
      Eq (α := Submodule pres.Ring ↥pres.ker)
        (Submodule.span pres.Ring
          (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
        ⊤),
    φ.range = ⊤
⊢ Function.Surjective (α := σ →₀ S) (β := pres.toExtension.Cotangent) (⇑φ : (a : σ →₀ S) → pres.toExtension.Cotangent)

Tactic:
rw [← LinearMap.range_eq_top] at h₁ ⊢

Premises used: LinearMap.range_eq_top
-- 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₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
rw :
  Submodule.map Extension.Cotangent.mk
      (Submodule.span pres.Ring
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) ≤
    φ.range
⊢ φ.range = ⊤

Tactic:
rw [← top_le_iff, ← h₁, LinearMap.range_eq_map, ← h₂]

Premises used: top_le_iff, LinearMap.range_eq_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 ι σ
φ : 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₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
rw :
  ∀ (m : ↥pres.toExtension.ker),
    Membership.mem (γ := Set ↥pres.toExtension.ker)
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) m →
      Membership.mem (α := pres.toExtension.Cotangent) φ.range
        (((Extension.Cotangent.mk :
                LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
                  pres.toExtension.Cotangent) :
              (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
            m :
          pres.toExtension.Cotangent)
⊢ Submodule.map (R := pres.Ring) (M := ↥pres.toExtension.ker) (σ₁₂ := RingHom.id pres.Ring) Extension.Cotangent.mk
      (Submodule.span pres.Ring
        (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯)) ≤
    φ.range

Tactic:
rw [Submodule.map_span_le]

Premises used: Submodule.map_span_le
-- 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₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
r : σ
⊢ ∃ (y : σ →₀ S),
    Eq (α := pres.toExtension.Cotangent)
      ((φ : (a : σ →₀ S) → pres.toExtension.Cotangent) y : pres.toExtension.Cotangent)
      (((Extension.Cotangent.mk :
              LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
                pres.toExtension.Cotangent) :
            (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
        pres.toExtension.Cotangent)

Tactic:
⟨Finsupp.single r 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat, Finsupp.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 ι σ
φ : 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₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
r : σ
refine :
  Eq (α := pres.toExtension.Cotangent)
    ((φ : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1) : pres.toExtension.Cotangent)
    (((Extension.Cotangent.mk :
            LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
              pres.toExtension.Cotangent) :
          (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
      pres.toExtension.Cotangent)
⊢ ∃ (y : σ →₀ S),
    Eq (α := pres.toExtension.Cotangent)
      ((φ : (a : σ →₀ S) → pres.toExtension.Cotangent) y : pres.toExtension.Cotangent)
      (((Extension.Cotangent.mk :
              LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
                pres.toExtension.Cotangent) :
            (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
        pres.toExtension.Cotangent)

Tactic:
refine ⟨Finsupp.single r 1, ?_⟩
-- 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₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
r : σ
simp :
  Eq (α := 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)
    (((Extension.Cotangent.mk :
            LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
              pres.toExtension.Cotangent) :
          (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
      pres.toExtension.Cotangent)
⊢ Eq (α := pres.toExtension.Cotangent)
    ((φ : (a : σ →₀ S) → pres.toExtension.Cotangent) (Finsupp.single r 1) : pres.toExtension.Cotangent)
    (((Extension.Cotangent.mk :
            LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
              pres.toExtension.Cotangent) :
          (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
      pres.toExtension.Cotangent)

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ]

Premises used: LinearMap.coe_mk, Algebra.Presentation.differentials.hom₁_single, AddHom.coe_mk
-- 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₁ : Eq (α := Submodule pres.toExtension.Ring pres.toExtension.Cotangent) (LinearMap.range Extension.Cotangent.mk) ⊤
h₂ :
  Eq (α := Submodule pres.Ring ↥pres.ker)
    (Submodule.span pres.Ring
      (Set.range fun (r : σ) ↦ Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯))
    ⊤
r : σ
⊢ Eq (α := 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)
    (((Extension.Cotangent.mk :
            LinearMap (R := pres.toExtension.Ring) (RingHom.id pres.toExtension.Ring) (↥pres.toExtension.ker)
              pres.toExtension.Cotangent) :
          (a : ↥pres.toExtension.ker) → pres.toExtension.Cotangent)
        (Subtype.mk (p := fun (x : pres.Ring) ↦ x ∈ pres.ker) (pres.relation r) ⋯) :
      pres.toExtension.Cotangent)

Tactic:
rfl
-- 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 : σ
simp :
  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)
⊢ 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.relation r) :
      pres.toExtension.CotangentSpace)

Tactic:
simp only [hom₁, Finsupp.linearCombination_single, one_smul, differentialsRelations,
    Basis.repr_symm_apply, Extension.cotangentComplex_mk]

Premises used: Algebra.Presentation.differentials.hom₁, Finsupp.linearCombination_single, one_smul, Algebra.Presentation.differentialsRelations, Module.Basis.repr_symm_apply, Algebra.Extension.cotangentComplex_mk
-- 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 : σ
h :
  ∀ (a : ι),
    Eq.{v + 1} (α := S)
      ((((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
                (1 ⊗ₜ[pres.toExtension.Ring]
                  (D R pres.toExtension.Ring : (a : pres.toExtension.Ring) → Ω[pres.toExtension.Ring⁄R])
                    (pres.relation r)) :
              ι →₀ S) :
            (a : ι) → S)
          a :
        S)
      ((((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
                ((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))))) :
              ι →₀ S) :
            (a : ι) → S)
          a :
        S)
⊢ Eq (α := ι →₀ S)
    ((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
        (1 ⊗ₜ[pres.toExtension.Ring]
          (D R pres.toExtension.Ring : (a : pres.toExtension.Ring) → Ω[pres.toExtension.Ring⁄R]) (pres.relation r)) :
      ι →₀ S)
    ((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
        ((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))))) :
      ι →₀ S)

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 ι σ
r : σ
a : ι
⊢ Eq.{v + 1} (α := S)
    ((((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
              (1 ⊗ₜ[pres.toExtension.Ring]
                (D R pres.toExtension.Ring : (a : pres.toExtension.Ring) → Ω[pres.toExtension.Ring⁄R])
                  (pres.relation r)) :
            ι →₀ S) :
          (a : ι) → S)
        a :
      S)
    ((((pres.cotangentSpaceBasis.repr : (a : pres.toExtension.CotangentSpace) → ι →₀ S)
              ((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))))) :
            ι →₀ S) :
          (a : ι) → S)
        a :
      S)

Tactic:
simp