awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((@ConcreteCategory.hom _ (moduleCategory R₂)
            (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
            (fun (X Y : ModuleCat R₂) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                  (↑Y : Type (max u_1 u₁))))
            _ _ _
            (((extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom ≫
                  (extendScalars f₁₂).whiskerLeft (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ≫
                    (extendScalars f₁₂).rightUnitor.hom).app
              M) :
          (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((@ConcreteCategory.hom _ (moduleCategory R₂)
            (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
            (fun (X Y : ModuleCat R₂) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                  (↑Y : Type (max u_1 u₁))))
            _ _ _ (NatTrans.app (𝟙 (extendScalars (RingHom.comp (RingHom.id R₂) f₁₂))) M) :
          (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
have w : Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
  ((Hom.hom (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ((extendScalars f₁₂).obj M)) :
        (a : (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁))) →
          (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
      ((Hom.hom ((extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom.app M) :
          (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m)) :
    (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
  (1 ⊗ₜ[R₁] m :
    (↑((restrictScalars (RingHom.comp (RingHom.id R₂) f₁₂)).obj (of R₂ R₂)) : Type u₁) ⊗[R₁] (↑M : Type (max u_1 u₁)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((Hom.hom (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ((extendScalars f₁₂).obj M)) :
          (a : (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        ((Hom.hom ((extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom.app M) :
            (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    (1 ⊗ₜ[R₁] m :
      (↑((restrictScalars (RingHom.comp (RingHom.id R₂) f₁₂)).obj (of R₂ R₂)) : Type u₁) ⊗[R₁] (↑M : Type (max u_1 u₁)))
have w : Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁))) (1 ⊗ₜ[R₁] m) (1 ⊗ₜ[R₁] m)
Tactic: erw [extendScalarsComp_hom_app_one_tmul f₁₂ (RingHom.id R₂) M m,
    extendScalarsId_hom_app_one_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Colimits (goal)
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y :=
      colimit
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
      (colimit.ι
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
        j)
      (AddCommGrpCat.ofHom (↑(Hom.hom m) : (↑(mkOfSMul' (coconePointSMul F)) : Type w') →+ (↑s.pt : Type w'))))
    (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))
have a : Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
  (CategoryStruct.comp (Y :=
    colimit
      (F ⋙
        forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
          (CD := AddCommGrpCat.carrier)))
    (colimit.ι
      (F ⋙
        forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
          (CD := AddCommGrpCat.carrier))
      j)
    (AddCommGrpCat.ofHom (↑(Hom.hom m) : (↑(mkOfSMul' (coconePointSMul F)) : Type w') →+ (↑s.pt : Type w'))))
  (AddCommGrpCat.ofHom (↑(Hom.hom ((colimitCocone F).ι.app j ≫ m)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Colimits (goal)
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type w
inst_2 : CommRing R
M ι : Type u
inst_3 : AddCommGroup M
inst_4 : Module R M
s : Cocone (J := Discrete ι) (C := ModuleCat.{u, w} R) (Discrete.functor fun (x : ι) ↦ of R M)
f : Cocone.pt (F := Discrete.functor fun (x : ι) ↦ of R M) (finsuppCocone R M ι) ⟶ s.pt
h : ∀ (j : Discrete ι), NatTrans.app (Cocone.ι (finsuppCocone R M ι)) j ≫ f = s.ι.app j
⊢ f =
    ↟((Finsupp.lsum R : (a : ι → M →ₗ[R] (↑s.pt : Type u)) → (ι →₀ M) →ₗ[R] (↑s.pt : Type u)) fun (i : ι) ↦
        Hom.hom (s.ι.app { as := i }))
have hf : Hom.hom f =
  Hom.hom
    (↟((Finsupp.lsum R : (a : ι → M →ₗ[R] (↑s.pt : Type u)) → (ι →₀ M) →ₗ[R] (↑s.pt : Type u)) fun (i : ι) ↦
        Hom.hom (s.ι.app { as := i })))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (hypothesis)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (tensorLeft ((restrictScalars f).obj (of B B)))
have algebraizeInst : Module.Flat A B
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (goal)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.Flat A B
⊢ PreservesFiniteLimits (tensorLeft ((restrictScalars f).obj (of B B)))
have change : PreservesFiniteLimits (C := ModuleCat A) (tensorLeft (of A B))
Tactic: change PreservesFiniteLimits <| tensorLeft (ModuleCat.of A B)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (hypothesis)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (extendScalars f)
have this : PreservesFiniteLimits (extendScalars f ⋙ restrictScalars f)
Tactic: have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) :=
    ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat hf
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (goal)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ (extendScalars f).ReflectsIsomorphisms
have refine : ∀ {M N : ModuleCat A} (g : M ⟶ N) (h : IsIso ((extendScalars f).map g)), IsIso g
Tactic: refine ⟨fun {M N} g h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (hypothesis)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h : IsIso ((extendScalars f).map g)
⊢ IsIso g
have algebraizeInst : Module.FaithfullyFlat A B
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (goal)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h : IsIso ((extendScalars f).map g)
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat A B
⊢ IsIso g
have rw : ∀
  (h :
    Function.Bijective (α := (↑((extendScalars f).obj M) : Type u)) (β := (↑((extendScalars f).obj N) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat B) ↦ (↑x1 : Type u) →ₗ[B] (↑x2 : Type u)) (CC := carrier)
            ((extendScalars f).map g)) :
        (a : (↑((extendScalars f).obj M) : Type u)) → (↑((extendScalars f).obj N) : Type u))),
  Module.FaithfullyFlat A B →
    Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat A) ↦ (↑x1 : Type u) →ₗ[A] (↑x2 : Type u)) (CC := carrier)
            g) :
        (a : (↑M : Type u)) → (↑N : Type u))
Tactic: rw [ConcreteCategory.isIso_iff_bijective] at h ⊢
Cleared hypotheses: h, algInst, algebraizeInst
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (hypothesis)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h :
  Function.Bijective (α := (↑((extendScalars f).obj M) : Type u)) (β := (↑((extendScalars f).obj N) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat B) ↦ (↑x1 : Type u) →ₗ[B] (↑x2 : Type u)) (CC := carrier)
          ((extendScalars f).map g)) :
      (a : (↑((extendScalars f).obj M) : Type u)) → (↑((extendScalars f).obj N) : Type u))
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat A B
⊢ Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat A) ↦ (↑x1 : Type u) →ₗ[A] (↑x2 : Type u)) (CC := carrier) g) :
      (a : (↑M : Type u)) → (↑N : Type u))
have h₁ : Function.Bijective (α := TensorProduct A B (↑M : Type u)) (β := TensorProduct A B (↑N : Type u))
  (⇑(LinearMap.lTensor B (Hom.hom g)) : (a : TensorProduct A B (↑M : Type u)) → TensorProduct A B (↑N : Type u))
Tactic: replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (goal)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat A B
h :
  Function.Bijective (α := TensorProduct A B (↑M : Type u)) (β := TensorProduct A B (↑N : Type u))
    (⇑(LinearMap.lTensor B (Hom.hom g)) : (a : TensorProduct A B (↑M : Type u)) → TensorProduct A B (↑N : Type u))
⊢ Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat A) ↦ (↑x1 : Type u) →ₗ[A] (↑x2 : Type u)) (CC := carrier) g) :
      (a : (↑M : Type u)) → (↑N : Type u))
have rwa : ∀
  (h :
    Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u)) (⇑(Hom.hom g) : (a : (↑M : Type u)) → (↑N : Type u))),
  Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat A) ↦ (↑x1 : Type u) →ₗ[A] (↑x2 : Type u)) (CC := carrier) g) :
      (a : (↑M : Type u)) → (↑N : Type u))
Tactic: rwa [Module.FaithfullyFlat.lTensor_bijective_iff_bijective] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (hypothesis)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ ComonadicLeftAdjoint (extendScalars f)
have this : PreservesFiniteLimits (extendScalars f)
Tactic: have := preservesFiniteLimits_extendScalars_of_flat hf.flat
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (hypothesis)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this : PreservesFiniteLimits (extendScalars f)
⊢ ComonadicLeftAdjoint (extendScalars f)
have this₁ : (extendScalars f).ReflectsIsomorphisms
Tactic: have := reflectsIsomorphisms_extendScalars_of_faithfullyFlat hf
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (goal)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this_1 : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ ComonadicLeftAdjoint (extendScalars f)
have convert_1 : HasEqualizerOfIsCosplitPair (extendScalars f)
Tactic: convert!
    Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
      (extendRestrictScalarsAdj f)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Descent (goal)
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this_1 : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
convert_1 : HasEqualizerOfIsCosplitPair (extendScalars f)
⊢ ComonadicLeftAdjoint (extendScalars f)
have convert_2 : PreservesLimitOfIsCosplitPair (extendScalars f)
Tactic: convert!
    Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
      (extendRestrictScalarsAdj f)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
a : (↑A : Type u)
b : (↑B : Type u)
⊢ d (a • b) =
    HSMul.hSMul (α := (↑A : Type u))
      ((RingHom.id (↑A : Type u) : (a : (↑A : Type u)) → (↑A : Type u)) a : (↑A : Type u)) (d b)
have dsimp : d (a • b) = a • d b
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
a : (↑A : Type u)
b : (↑B : Type u)
⊢ d (a • b) = a • d b
have rw : HSMul.hSMul (α := (↑B : Type u)) ((CommRingCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
    (d b) =
  a • d b
Tactic: rw [RingHom.smul_toAlgebra, d_mul, d_map, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
⊢ Eq.{v + 1} (α := (↑M : Type v))
    ((({ toFun := d, map_add' := d_add, map_smul' := ⋯ } :
          LinearMap.{u, u, u, v} (R := (↑A : Type u)) (RingHom.id (↑A : Type u)) (↑B : Type u) (↑M : Type v)) :
        (a : (↑B : Type u)) → (↑M : Type v))
      1)
    0
have dsimp : d 1 = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
⊢ d 1 = 0
have rw : d ((CommRingCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) 1) = 0
Tactic: rw [← f.hom.map_one, d_map]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
rw : d ((CommRingCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) 1) = 0
⊢ d 1 = 0
have rw₁ : Eq.{v + 1} (α := (↑M : Type v)) 0 0
Tactic: rw [← f.hom.map_one, d_map]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
⊢ α = β
have rw : α - β = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
⊢ ⊤ ≤ (ModuleCat.Hom.hom (α - β)).ker
have rw : Set.range (ι := (↑B : Type u))
    (⇑(_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u)) :
      (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)]) ⊆
  (↑(ModuleCat.Hom.hom (α - β)).ker : Set Ω[(↑B : Type u)⁄(↑A : Type u)])
Tactic: rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
y : (↑B : Type u)
⊢ Membership.mem (α := Ω[(↑B : Type u)⁄(↑A : Type u)])
    (↑(ModuleCat.Hom.hom (α - β)).ker : Set Ω[(↑B : Type u)⁄(↑A : Type u)])
    ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) : (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
        y :
      Ω[(↑B : Type u)⁄(↑A : Type u)])
have rw : Eq (α := (↑M : Type u))
  ((ModuleCat.Hom.hom α : (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → (↑M : Type u))
      ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) : (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
          y :
        Ω[(↑B : Type u)⁄(↑A : Type u)]) :
    (↑M : Type u))
  ((ModuleCat.Hom.hom β : (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → (↑M : Type u))
      ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) : (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
          y :
        Ω[(↑B : Type u)⁄(↑A : Type u)]) :
    (↑M : Type u))
Tactic: rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]