mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ ∫ (x : ℝ) in ↑i..↑(i + 1), f ↑i ≤ ∫ (x : ℝ) in ↑i..↑(i + 1), g x

Tactic:
apply integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
i : ℕ
hi : i ∈ Finset.Ico a b
x : ℝ
hx : x ∈ Ioo ↑i ↑(i + 1)
⊢ f ↑i ≤ g x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
i : ℕ
hi : i ∈ Finset.Ico a b
x : ℝ
hx : x ∈ Ioo ↑i ↑(i + 1)
⊢ i ∈ Ico a b

Tactic:
by simpa using hi

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
⊢ n ∈ Set.Ioi 0 → d < u n / ↑n

Tactic:
npos

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < u n / ↑n
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
ι✝ : Type u_2
inst✝⁵ : HasProductsOfShape ι✝ C
inst✝⁴ : HasProducts C
inst✝³ : HasFilteredColimitsOfSize.{w, w, v_1, u_1} C
inst✝² : IsIPC C
ι : Type u_3
inst✝¹ : Small.{w, u_3} ι
inst✝ : HasProductsOfShape ι C
⊢ IsIPCOfShape.{w, u_3, v_1, u_1} ι C

Tactic:
suffices IsIPCOfShape (Shrink.{w} ι) C from .of_equiv (equivShrink ι).symm

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
ι✝ : Type u_2
inst✝⁵ : HasProductsOfShape ι✝ C
inst✝⁴ : HasProducts C
inst✝³ : HasFilteredColimitsOfSize.{w, w, v_1, u_1} C
inst✝² : IsIPC C
ι : Type u_3
inst✝¹ : Small.{w, u_3} ι
inst✝ : HasProductsOfShape ι C
⊢ IsIPCOfShape.{w, w, v_1, u_1} (Shrink.{w, u_3} ι) C
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv - g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯
          ⋯))

Tactic:
Cocycle.fromSingleMk_sub _ _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hg])

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯ -
          Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯
              (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
            ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              ((Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯).postcomp φ.hom'))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯

Tactic:
Cocycle.equivHomShift_symm_postcomp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯
              (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
            ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯) ≫
              (shiftFunctor (CochainComplex C ℤ) ↑n).map φ.hom')
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          ((inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y) ≫
            (DerivedCategory.singleFunctor C 0).map g))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        ((ShiftedHom.mk₀ 0 ⋯ (DerivedCategory.Q.map φ.hom')).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
          ⋯)
        ⋯)
      ⋯

Tactic:
ShiftedHom.mk₀_comp_mk₀

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          ((inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y) ≫
            (DerivedCategory.singleFunctor C 0).map g))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map φ.hom' ≫
            inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              ((Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯).postcomp
                ((singleFunctor C 0).map g)))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y')) ⋯)
      ⋯

Tactic:
Cocycle.equivHomShift_symm_postcomp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯) ≫
              (shiftFunctor (CochainComplex C ℤ) ↑n).map ((singleFunctor C 0).map g))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y')) ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso
    (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).liftCycles (F.map (𝟙 X)) 1
      toRightDerivedZero'._proof_1 ⋯)

Tactic:
CochainComplex.isIso_liftCycles_iff

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ { X₁ := F.obj X, X₂ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 0,
        X₃ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 1,
        f := F.map (𝟙 X),
        g := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).d 0 1,
        zero := ⋯ }.Exact ∧
    Mono (F.map (𝟙 X))
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ ((ShiftedHom.mk₀ ↑0 ⋯
              ((DerivedCategory.singleFunctor C 0).map g ≫
                (DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          (ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯ =
    (((ShiftedHom.mk₀ 0 ⋯
                  ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
              (ShiftedHom.mk₀ 0 ⋯ (DerivedCategory.Q.map φ.hom')) ⋯).comp
          (ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯

Tactic:
ShiftedHom.mk₀_comp_mk₀

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ ((ShiftedHom.mk₀ ↑0 ⋯
              ((DerivedCategory.singleFunctor C 0).map g ≫
                (DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          (ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯ =
    ((ShiftedHom.mk₀ 0 ⋯
              (((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π')) ≫
                DerivedCategory.Q.map φ.hom')).comp
          (ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q)
          ⋯).comp
      (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Nonempty
    (IsLimit
      (KernelFork.ofι
        { X₁ := F.obj X, X₂ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 0,
            X₃ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 1, f := F.map (P.ι.f 0),
            g := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).d 0 1, zero := ⋯ }.f
        ⋯))

Tactic:
exact ⟨KernelFork.mapIsLimit _ (P.isLimitKernelFork) F⟩

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
g : G
⊢ (s.pt.ρ g ≫ ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) =
    (↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) ≫
      { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt.ρ
        g

Tactic:
ext x
            funext j
            exact ConcreteCategory.congr_hom ((s.π.app ⟨j⟩).comm g) x

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ SingleObj G ⥤ V
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_evaluation

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ SingleObj G ⥤ V
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ ∀ (k : SingleObj G), PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj k)
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Mono η
⊢ ∀ (c : C), Mono (η.app c)

Tactic:
c

Goal state after:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Mono η
c : C
⊢ Mono (η.app c)
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Epi η
⊢ ∀ (c : C), Epi (η.app c)

Tactic:
c

Goal state after:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Epi η
c : C
⊢ Epi (η.app c)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ adj₂.unit.app Y ≫
        U'.map ((L ⋙ F).map f) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    adj₂.unit.app Y ≫ U'.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        ((adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))).symm (f ≫ U'.map (F.map (adj₁.unit.app X))))

Tactic:
adj₂.homEquiv_counit

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ adj₂.unit.app Y ≫
        U'.map ((L ⋙ F).map f) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    adj₂.unit.app Y ≫ U'.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((L ⋙ F).map f ≫ adj₂.counit.app (F.obj X)))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        ((adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))).symm (f ≫ U'.map (F.map (adj₁.unit.app X))))
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
x✝ : Cᵒᵖ
⊢ t.op.rightToLeft.app x✝ = (NatTrans.op t.rightToLeft).app x✝

Tactic:
rightToLeft_eq_units,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
x✝ : Cᵒᵖ
⊢ (F.op.leftUnitor.inv ≫
          whiskerRight t.op.adj₁.unit F.op ≫
            (H.op.associator G.op F.op).hom ≫ inv (H.op.whiskerLeft t.op.adj₂.unit) ≫ H.op.rightUnitor.hom).app
      x✝ =
    (NatTrans.op t.rightToLeft).app x✝
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
⊢ ∀ {c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv

Tactic:
c

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
⊢ ∀ (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv