awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
n : ℕ
x : Ext.{w, v, u} X Y n
r : R
inst_5 : HasDerivedCategory.{u_1, v, u} C
⊢ (r • x).hom =
    HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r x.hom

Tactic:
simp [smul_eq_comp_mk₀]

Premises used: CategoryTheory.Abelian.Ext.smul_eq_comp_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y Z : C
a b : ℕ
α : Ext.{w, v, u} X Y a
β : Ext.{w, v, u} Y Z b
c : ℕ
h : a + b = c
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (r • β) h = r • α.comp β h

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y Z : C
a b : ℕ
α : Ext.{w, v, u} X Y a
β : Ext.{w, v, u} Y Z b
c : ℕ
h : a + b = c
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (r • α).comp β h = r • α.comp β h

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_5 : HasDerivedCategory.{w', v, u} C
⊢ ∀ (m : R) (x : Ext.{w, v, u} X Y n),
    Equiv.toFun (AddEquiv.toEquiv homAddEquiv) (m • x) =
      HSMul.hSMul (α := R) (β :=
        ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        ((RingHom.id R : (a : R) → R) m : R) (Equiv.toFun (AddEquiv.toEquiv homAddEquiv) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
r : R
f : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ (r • f) = HSMul.hSMul (β := Ext.{w, v, u} X Y 0) r (mk₀ f)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
n : ℕ
m : R
x : Ext.{w, v, u} X Y 0
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y 0)
    ((Equiv.symm homEquiv₀ : (a : X ⟶ Y) → Ext X Y 0) (Equiv.toFun (AddEquiv.toEquiv addEquiv₀) (m • x)) :
      Ext.{w, v, u} X Y 0)
    ((Equiv.symm homEquiv₀ : (a : X ⟶ Y) → Ext X Y 0)
        (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (Equiv.toFun (AddEquiv.toEquiv addEquiv₀) x)) :
      Ext.{w, v, u} X Y 0)

Tactic:
simp [mk₀_smul]

Premises used: CategoryTheory.Abelian.Ext.mk₀_smul
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
f : Ext.{w, v, u} X Y 0
⊢ mk₀ ((linearEquiv₀ : (a : Ext X Y 0) → X ⟶ Y) f) = f

Tactic:
addEquiv₀.left_inv f

Premises used: CategoryTheory.Localization.SmallHom.mk, Function.surjInv, CategoryTheory.Localization.SmallShiftedHom.mk₀, Classical.choose, AddEquiv.toEquiv, CategoryTheory.Abelian.Ext.addEquiv₀, CategoryTheory.Localization.SmallShiftedHom.mk, CategoryTheory.Abelian.Ext.mk₀, Equiv.left_inv
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
R : Type t
inst_3 : CommRing R
inst_4 : Linear.{t, v, u} R C
X Y Z : C
a b c : ℕ
h : a + b = c
α : Ext.{w, v, u} X Y a
⊢ ∀ (x y : Ext.{w, v, u} Y Z b), α.comp (x + y) h = α.comp x h + α.comp y h

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
R : Type t
inst_3 : CommRing R
inst_4 : Linear.{t, v, u} R C
X Y Z : C
a b c : ℕ
h : a + b = c
α : Ext.{w, v, u} X Y a
⊢ ∀ (m : R) (x : Ext.{w, v, u} Y Z b),
    α.comp (m • x) h = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (α.comp x h)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
R : Type t
inst_3 : CommRing R
inst_4 : Linear.{t, v, u} R C
X Y Z : C
a b c : ℕ
h : a + b = c
⊢ ∀ (x y : Ext.{w, v, u} X Y a),
    { toFun := fun (β : Ext.{w, v, u} Y Z b) ↦ (x + y).comp β h, map_add' := ⋯, map_smul' := ⋯ } =
      HAdd.hAdd (α := Ext.{w, v, u} Y Z b →ₗ[R] Ext.{w, v, u} X Z c)
        { toFun := fun (β : Ext.{w, v, u} Y Z b) ↦ x.comp β h, map_add' := ⋯, map_smul' := ⋯ :
          Ext.{w, v, u} Y Z b →ₗ[R] Ext.{w, v, u} X Z c }
        { toFun := fun (β : Ext.{w, v, u} Y Z b) ↦ y.comp β h, map_add' := ⋯, map_smul' := ⋯ :
          Ext.{w, v, u} Y Z b →ₗ[R] Ext.{w, v, u} X Z c }

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
R : Type t
inst_3 : CommRing R
inst_4 : Linear.{t, v, u} R C
X Y Z : C
a b c : ℕ
h : a + b = c
⊢ ∀ (m : R) (x : Ext.{w, v, u} X Y a),
    { toFun := fun (β : Ext.{w, v, u} Y Z b) ↦ (m • x).comp β h, map_add' := ⋯, map_smul' := ⋯ } =
      HSMul.hSMul (α := R) (β := Ext.{w, v, u} Y Z b →ₗ[R] Ext.{w, v, u} X Z c) ((RingHom.id R : (a : R) → R) m : R)
        { toFun := fun (β : Ext.{w, v, u} Y Z b) ↦ x.comp β h, map_add' := ⋯, map_smul' := ⋯ :
          Ext.{w, v, u} Y Z b →ₗ[R] Ext.{w, v, u} X Z c }

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasDerivedCategory.{t, v, u} C
inst_8 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
⊢ QuasiIso (CochainComplex.mappingCone.descShortComplex S)

Tactic:
have := CochainComplex.mappingCone.quasiIso_descShortComplex hS
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasDerivedCategory.{t, v, u} C
inst_8 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj Q (CochainComplex.mappingCone S.f)))
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁))))
    (Functor.map F.mapDerivedCategory (Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
      Functor.map F.mapDerivedCategory (NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁))
    (Functor.map F.mapDerivedCategory (Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
      NatTrans.app (Iso.hom F.mapDerivedCategoryFactors)
          (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1)
            (CochainComplex.mappingCone.triangle S.f).obj₁) ≫
        CategoryStruct.comp (Y :=
          Functor.obj Q
            (Functor.obj (shiftFunctor (CochainComplex.{v', u', 0} D ℤ) (A := ℤ) 1)
              (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
          (Functor.map Q
            (NatTrans.app (Iso.hom (Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1)) S.X₁))
          (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
              (Functor.obj Q (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
            (NatTrans.app (Iso.hom (Functor.commShiftIso Q 1))
              (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁))
            (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors) S.X₁) ≫
              NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1)) (Functor.obj Q S.X₁))))

Tactic:
simp [NatTrans.shift_app, Functor.commShiftIso_comp_hom_app, Functor.commShiftIso_comp_inv_app,
    ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Functor.commShiftIso_comp_inv_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.shift_app
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
inst_4 : HasDerivedCategory.{t, v, u} C
inst_5 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
F : Functor.{v, v', u, u'} C D
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
pf : HasZeroObject.{v, u} C
pf_1 : IsRightCancelAdd ℤ
pf_2 : IsRightCancelAdd ℤ
pf_3 : F.PreservesZeroMorphisms
pf_4 :
  Functor.PreservesZeroMorphisms (D := CochainComplex.{v, u, 0} C ℤ) (HomologicalComplex.single C (ComplexShape.up ℤ) 0)
pf_5 :
  Functor.PreservesZeroMorphisms (C := CochainComplex.{v, u, 0} C ℤ) (D := CochainComplex.{v', u', 0} D ℤ)
    (F.mapHomologicalComplex (ComplexShape.up ℤ))
h1 :
  ShortExact (C := CochainComplex.{v', u', 0} D ℤ)
    (ShortComplex.map (C := CochainComplex.{v, u, 0} C ℤ) (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))
      (F.mapHomologicalComplex (ComplexShape.up ℤ)))
pf_6 : HasZeroObject.{v', u'} D
pf_7 :
  Functor.PreservesZeroMorphisms (D := CochainComplex.{v', u', 0} D ℤ)
    (HomologicalComplex.single D (ComplexShape.up ℤ) 0)
h2 :
  ShortExact (C := CochainComplex.{v', u', 0} D ℤ)
    (ShortComplex.map (S.map F) (HomologicalComplex.single D (ComplexShape.up ℤ) 0))
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D) (Functor.obj (singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
        (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))
    (Functor.map Q
        (CategoryStruct.comp (Y :=
          Functor.obj (C := CochainComplex.{v, u, 0} C ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (Functor.obj (CochainComplex.singleFunctor C 0) S.X₃))
          (NatTrans.app (Iso.inv (F.mapCochainComplexSingleFunctor 0)) S.X₃ :
            Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
              (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) S.X₃)
              (Functor.obj
                (Functor.comp (D := CochainComplex.{v, u, 0} C ℤ) (CochainComplex.singleFunctor C 0)
                  (F.mapHomologicalComplex (ComplexShape.up ℤ)))
                S.X₃))
          (NatTrans.app (Iso.hom (F.mapCochainComplexSingleFunctor 0)) S.X₃ :
            Quiver.Hom (V := CochainComplex.{v', u', 0} D ℤ)
              (Functor.obj
                (Functor.comp (D := CochainComplex.{v, u, 0} C ℤ) (CochainComplex.singleFunctor C 0)
                  (F.mapHomologicalComplex (ComplexShape.up ℤ)))
                S.X₃)
              (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) S.X₃))) ≫
      triangleOfSESδ h2)
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors D) 0) (F.obj S.X₃)) ≫
      triangleOfSESδ h2 ≫
        Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (𝟙 (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
inst_4 : HasDerivedCategory.{t, v, u} C
inst_5 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
F : Functor.{v, v', u, u'} C D
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
⊢ Eq.{t' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{t', v', u'} D) (M := ℤ)
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory (Functor.obj (singleFunctor C 0) S.X₃))
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory (Functor.obj (singleFunctor C 0) S.X₁)) 1)
    (ShiftedHom.map hS.singleδ F.mapDerivedCategory)
    (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₃ ≫
      singleδ ⋯ ≫
        Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₁))

Tactic:
simp [← hS.mapShiftedHom_singleδ'_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
h : HasExt.{w', v', u'} D
X Y : C
⊢ HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
    (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) ℤ (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) X)
    (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) Y)

Tactic:
h (F.obj X) (F.obj Y)

Premises used: CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) n) (mapExactFunctor.{w, w', u, u', v, v'} F 0) 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
f g : Ext.{w, v, u} X Y n
⊢ mapExactFunctor F (f + g) =
    HAdd.hAdd (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) n) (mapExactFunctor F f) (mapExactFunctor F g)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X_1 Y_1 : C
n_1 : ℕ
X Y : C
n : ℕ
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) n) (Ext.mapExactFunctor.{w, w', u, u', v, v'} F 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X_1 Y_1 : C
n_1 : ℕ
X Y : C
n : ℕ
⊢ ∀ (x y : Ext.{w, v, u} X Y n),
    Ext.mapExactFunctor F (x + y) =
      HAdd.hAdd (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) n) (Ext.mapExactFunctor F x) (Ext.mapExactFunctor F y)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
⊢ Eq (α := (a : Ext.{w, v, u} X Y n) → Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
    (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n) (Ext.mapExactFunctor F)

Tactic:
rfl

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.LocalizerMorphism.smallHomMap', CategoryTheory.LocalizerMorphism.smallShiftedHomMap, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
e : Ext.{w, v, u} X Y n
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
    ((F.mapExtAddHom X Y n : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n) e : Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
    (Ext.mapExactFunctor F e : Ext.{w', v', u'} (F.obj X) (F.obj Y) n)

Tactic:
rfl

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.LocalizerMorphism.smallHomMap', CategoryTheory.LocalizerMorphism.smallShiftedHomMap, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v, u} R C
inst_11 : CategoryTheory.Linear.{u_1, v', u'} R D
inst_12 : Linear R F
r : R
f : Ext.{w, v, u} X Y n
⊢ Ext.mapExactFunctor F (r • f) = HSMul.hSMul (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n) r (Ext.mapExactFunctor F f)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X_1 Y_1 : C
n_1 : ℕ
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v, u} R C
inst_11 : CategoryTheory.Linear.{u_1, v', u'} R D
inst_12 : Linear R F
X Y : C
n : ℕ
⊢ ∀ (m : R) (x : Ext.{w, v, u} X Y n),
    ZeroHom.toFun (↑(F.mapExtAddHom X Y n) : ZeroHom (Ext X Y n) (Ext (F.obj X) (F.obj Y) n)) (m • x) =
      HSMul.hSMul (α := R) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n) ((RingHom.id R : (a : R) → R) m : R)
        (ZeroHom.toFun (↑(F.mapExtAddHom X Y n) : ZeroHom (Ext X Y n) (Ext (F.obj X) (F.obj Y) n)) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v, u} R C
inst_11 : CategoryTheory.Linear.{u_1, v', u'} R D
inst_12 : Linear R F
⊢ (↑(F.mapExtLinearMap R X Y n) : Ext X Y n →+ Ext (F.obj X) (F.obj Y) n) = F.mapExtAddHom X Y n

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CategoryTheory.Abelian.Ext.mapExactFunctor, CategoryTheory.Functor.mapExtAddHom, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.LocalizerMorphism.smallHomMap', CategoryTheory.LocalizerMorphism.smallShiftedHomMap, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v, u} R C
inst_11 : CategoryTheory.Linear.{u_1, v', u'} R D
inst_12 : Linear R F
⊢ Eq (α := (a : Ext.{w, v, u} X Y n) → Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
    (⇑(F.mapExtLinearMap R X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n) (Ext.mapExactFunctor F)

Tactic:
rfl

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.LocalizerMorphism.smallHomMap', CategoryTheory.LocalizerMorphism.smallShiftedHomMap, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v, u} R C
inst_11 : CategoryTheory.Linear.{u_1, v', u'} R D
inst_12 : Linear R F
e : Ext.{w, v, u} X Y n
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
    ((F.mapExtLinearMap R X Y n : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n) e :
      Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
    (Ext.mapExactFunctor F e : Ext.{w', v', u'} (F.obj X) (F.obj Y) n)

Tactic:
rfl

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.LocalizerMorphism.smallHomMap', CategoryTheory.LocalizerMorphism.smallShiftedHomMap, rfl