awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : P.Cotangent
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent) (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) x))
    (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) x))
have h : ∀ (x : ↥P.ker),
  Eq.{w' + 1} (α := P'.ker.Cotangent)
    (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
Tactic: obtain ⟨x, rfl⟩ := mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
have h : (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
      ((mk : (a : ↥P'.ker) → P'.Cotangent)
          (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
            (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry) :
        P'.Cotangent)
      ((mk : (a : ↥P'.ker) → P'.Cotangent)
          (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
            (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry) :
        P'.Cotangent)).val =
  (P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
    (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) (↑x : P.Ring))
Tactic: simp only [LinearMap.sub_apply, map_mk, LinearMap.coe_comp, Function.comp_apply,
    cotangentComplex_mk, Hom.sub_tmul, one_smul, val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
⊢ (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
        ((mk : (a : ↥P'.ker) → P'.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
          P'.Cotangent)
        ((mk : (a : ↥P'.ker) → P'.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
          P'.Cotangent)).val =
    (P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
      (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) (↑x : P.Ring))
have h : Eq (α := ↥P'.ker.cotangentIdeal)
  ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
      (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
          ((mk : (a : ↥P'.ker) → P'.Cotangent)
              (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry) :
            P'.Cotangent)
          ((mk : (a : ↥P'.ker) → P'.Cotangent)
              (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry) :
            P'.Cotangent)).val :
    ↥P'.ker.cotangentIdeal)
  ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
      ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
        (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker)
          (↑x : P.Ring))) :
    ↥P'.ker.cotangentIdeal)
Tactic: apply (Ideal.cotangentEquivIdeal _).injective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
⊢ Eq (α := ↥P'.ker.cotangentIdeal)
    ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
              P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
              P'.Cotangent)).val :
      ↥P'.ker.cotangentIdeal)
    ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
          (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker)
            (↑x : P.Ring))) :
      ↥P'.ker.cotangentIdeal)
have h : Eq.{w' + 1} (α := P'.Ring ⧸ HPow.hPow (β := ℕ) P'.ker 2)
  (↑((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry) :
              P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry) :
              P'.Cotangent)).val) :
    P'.Ring ⧸ P'.ker ^ 2)
  (↑((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
          (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker)
            (↑x : P.Ring)))) :
    P'.Ring ⧸ P'.ker ^ 2)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ Subsingleton.{u_1 + 1} ↥P.cotangentComplex.ker ↔
    Function.Injective (α := P.Cotangent) (β := P.CotangentSpace)
      (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace)
have rw : (∀ (y : ↥P.cotangentComplex.ker), y = 0) ↔ ∀ (x : ↥P.cotangentComplex.ker), (↑x : P.Cotangent) = 0
Tactic: rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff, subsingleton_iff_forall_eq 0, Subtype.forall']
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ Function.Exact (M := P.H1Cotangent) (N := P.Cotangent) (P := P.CotangentSpace)
    (⇑h1Cotangentι : (a : P.H1Cotangent) → P.Cotangent) (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace)
have rw : P.cotangentComplex.ker = LinearMap.range h1Cotangentι
Tactic: rw [LinearMap.exact_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
⊢ LinearMap.{v, v, u_1, w'} (RingHom.id S) P.H1Cotangent P'.H1Cotangent
have refine : ∀ (x : P.Cotangent) (hx : x ∈ P.cotangentComplex.ker),
  Membership.mem (α := P'.Cotangent) (γ := Submodule S P'.Cotangent)
    (Submodule.restrictScalars S P'.cotangentComplex.ker)
    ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x : P'.Cotangent)
Tactic: refine (Cotangent.map f).restrict (p := LinearMap.ker P.cotangentComplex)
    (q := (LinearMap.ker P'.cotangentComplex).restrictScalars S) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx : x ∈ P.cotangentComplex.ker
⊢ Membership.mem (α := P'.Cotangent) (γ := Submodule S P'.Cotangent)
    (Submodule.restrictScalars S P'.cotangentComplex.ker)
    ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x : P'.Cotangent)
have hx₁ : Eq (α := P.CotangentSpace) ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x : P.CotangentSpace)
  (0 : P.CotangentSpace)
Tactic: simp only [LinearMap.mem_ker, Submodule.restrictScalars_mem] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P.CotangentSpace) ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x : P.CotangentSpace)
    (0 : P.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    (0 : P'.CotangentSpace)
have hx₁ : Eq (α := P'.CotangentSpace)
  ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
      ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x) :
    P'.CotangentSpace)
  ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
Tactic: apply_fun (CotangentSpace.map f) at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    (0 : P'.CotangentSpace)
have hx₁ : Eq (α := P'.CotangentSpace)
  ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
      ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
    P'.CotangentSpace)
  ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
Tactic: rw [CotangentSpace.map_cotangentComplex] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    (0 : P'.CotangentSpace)
have rw : Eq (α := P'.CotangentSpace) ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0) 0
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f g : P.Hom P'
⊢ map f = map g
have h : ∀ (x : P.H1Cotangent),
  Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val (↑((map f : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))
    (Cotangent.val (↑((map g : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val (↑((map f : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))
    (Cotangent.val (↑((map g : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))
have h : Eq.{w' + 1} (α := P'.ker.Cotangent)
  (Cotangent.val ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))
  (Cotangent.val ((Cotangent.map g : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))
Tactic: simp only [map_apply_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))
    (Cotangent.val ((Cotangent.map g : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))
have h : Eq.{w' + 1} (α := P'.ker.Cotangent)
  (Cotangent.val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent))) 0
Tactic: rw [← sub_eq_zero, ← Cotangent.val_sub, ← LinearMap.sub_apply, Cotangent.map_sub_map]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ map (Hom.id P) = LinearMap.id
have h : ∀ (x : P.H1Cotangent),
  Eq.{u_1 + 1} (α := P.ker.Cotangent)
    (Cotangent.val (↑((map (Hom.id P) : (a : P.H1Cotangent) → P.H1Cotangent) x) : P.Cotangent))
    (Cotangent.val (↑((LinearMap.id : (a : P.H1Cotangent) → P.H1Cotangent) x) : P.Cotangent))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
P : Extension.{u_1, u, v} R S
f : P.Hom P'
g : P'.Hom P''
⊢ Eq (α := LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) (map (g.comp f))
    ((↑S :
          {S_1 : Type v'} →
            {M : Type w'} →
              {M₂ : Type w''} →
                [inst : Semiring S] →
                  [inst_23 : Semiring S_1] →
                    [inst_24 : AddCommMonoid M] →
                      [inst_25 : AddCommMonoid M₂] →
                        [inst_26 : Module S M] →
                          [inst_27 : Module S M₂] →
                            [inst_28 : Module S_1 M] →
                              [inst_29 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (map g) ∘ₗ
      map f)
have h : ∀ (x : P.H1Cotangent),
  Eq.{w'' + 1} (α := P''.ker.Cotangent)
    (Cotangent.val
      (↑(((map (g.comp f) : LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) :
              (a : P.H1Cotangent) → P''.H1Cotangent)
            x) :
        P''.Cotangent))
    (Cotangent.val
      (↑((((↑S :
                      {S_1 : Type v'} →
                        {M : Type w'} →
                          {M₂ : Type w''} →
                            [inst : Semiring S] →
                              [inst_23 : Semiring S_1] →
                                [inst_24 : AddCommMonoid M] →
                                  [inst_25 : AddCommMonoid M₂] →
                                    [inst_26 : Module S M] →
                                      [inst_27 : Module S M₂] →
                                        [inst_28 : Module S_1 M] →
                                          [inst_29 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    (map g) ∘ₗ
                  map f :
                LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) :
              (a : P.H1Cotangent) → P''.H1Cotangent)
            x) :
        P''.Cotangent))
Tactic: ext