mathlib-initiative/mathlib-tactics huggingface dataset:
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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : (fun x ↦ u (c x) / ↑(c x) - l) =o[atTop] fun _x ↦ 1
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)

Tactic:
Asymptotics.isLittleO_iff

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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
hM : 0 < M
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, ‖f x‖ = ∫ (x : ℝ) in ↑N..↑M + ↑N, f x

Tactic:
refine intervalIntegral.integral_congr_uIoo fun x ↦ ?_
        grind [Real.norm_of_nonneg, uIoo_of_le]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x✝ :
  (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ×'
    (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
      f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f'
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ g'
⊢ f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)

Tactic:
simp only [w, add_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } :=
  { τ₁ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁,
    τ₂ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂,
    τ₃ := ι { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ }.Exact

Tactic:
← ShortComplex.exact_iff_of_epi_of_isIso_of_mono α

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } :=
  { τ₁ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁,
    τ₂ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂,
    τ₃ := ι { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ShortComplex.QuasiIso
    ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
      (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩))

Tactic:
ShortComplex.quasiIso_iff_of_zeros

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
              ((CochainComplex.single₀ C).obj Z)).X₂,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
        X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
        f :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
              (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
        g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
        zero := ⋯ }.Exact ∧
    Mono
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
          (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂

case zero.hf₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).f = 0

case zero.hg₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).g = 0

case zero.hf₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).f = 0
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
σ τ : G
x : G ⧸ N
⊢ (ConcreteCategory.hom { hom := FintypeCat.homMk (Quotient.lift (fun σ_1 ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ }.hom) x =
    (ConcreteCategory.hom
        ({ hom := FintypeCat.homMk (Quotient.lift (fun σ_1 ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ } *
            { hom := FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ }).hom)
      x

Tactic:
induction x using Quotient.inductionOn with | _ x
     =>  _ 

Goal state after:
case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
σ τ x : G
⊢ (ConcreteCategory.hom { hom := FintypeCat.homMk (Quotient.lift (fun σ_1 ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ }.hom)
      ⟦x⟧ =
    (ConcreteCategory.hom
        ({ hom := FintypeCat.homMk (Quotient.lift (fun σ_1 ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ } *
            { hom := FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ }).hom)
      ⟦x⟧
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
this✝¹ : L.PreservesMonomorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Mono f✝
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
this : IsIso (L.map (Abelian.factorThruImage f))
⊢ (asIso (L.map (Abelian.factorThruImage f))).hom ≫ (Arrow.mk (L.map (Abelian.image.ι f))).hom =
    (Arrow.mk (L.map f)).hom ≫ (Iso.refl (Arrow.mk (L.map f)).right).hom

Tactic:
by simp [← L.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
this✝¹ : L.PreservesEpimorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Epi f✝
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
this : IsIso (L.map (Abelian.image.ι f))
⊢ (Iso.refl (Arrow.mk (L.map (Abelian.factorThruImage f))).left).hom ≫ (Arrow.mk (L.map f)).hom =
    (Arrow.mk (L.map (Abelian.factorThruImage f))).hom ≫ (asIso (L.map (Abelian.image.ι f))).hom

Tactic:
by simp [← L.map_comp]

Goal state after:
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
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
⊢ L'.IsLeftAdjoint

Tactic:
let : ∀ X, RegularMono ((Comonad.adj (comonadicAdjunction F).toComonad).unit.app X) := by
    intro X
    simp only [Comonad.adj_unit]
    exact ⟨_, _, _, _, Comonad.beckCoalgebraEqualizer X⟩

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
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this✝ : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
this : (X : (comonadicAdjunction F).toComonad.Coalgebra) →
  RegularMono ((comonadicAdjunction F).toComonad.adj.unit.app X) :=
  fun X ↦
    ⋯.mpr
      { Z := (comonadicAdjunction F).toComonad.cofree.obj ((comonadicAdjunction F).toComonad.obj X.A),
        left := Comonad.CofreeEqualizer.topMap X, right := Comonad.CofreeEqualizer.bottomMap X, w := ⋯,
        isLimit := Comonad.beckCoalgebraEqualizer X }
⊢ L'.IsLeftAdjoint
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.fiber =
    ({ base := f.base,
            fiber :=
              (α.app { as := op a.base }).toFunctor.map f.fiber ≫
                (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
          { base := g.base,
            fiber :=
              (α.app { as := op b.base }).toFunctor.map g.fiber ≫
                (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).fiber ≫
      eqToHom ⋯

Tactic:
simp only [categoryStruct_comp_base, op_comp, Quiver.Hom.comp_toLoc,
        categoryStruct_comp_fiber, Cat.Hom.comp_toFunctor, map_comp, naturality_comp_hom_app, assoc,
        eqToHom_refl, comp_id]

Goal state after:
case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ (α.app { as := op a.base }).toFunctor.map f.fiber ≫
      (α.app { as := op a.base }).toFunctor.map ((F.map f.base.op.toLoc).toFunctor.map g.fiber) ≫
        (α.app { as := op a.base }).toFunctor.map
            ((F.mapComp g.base.op.toLoc f.base.op.toLoc).inv.toNatTrans.app c.fiber) ≫
          (α.app { as := op a.base }).toFunctor.map
              ((F.mapComp g.base.op.toLoc f.base.op.toLoc).hom.toNatTrans.app c.fiber) ≫
            (α.naturality f.base.op.toLoc).hom.toNatTrans.app ((F.map g.base.op.toLoc).toFunctor.obj c.fiber) ≫
              (G.map f.base.op.toLoc).toFunctor.map ((α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber) ≫
                (G.mapComp g.base.op.toLoc f.base.op.toLoc).inv.toNatTrans.app
                  ((α.app { as := op c.base }).toFunctor.obj c.fiber) =
    (α.app { as := op a.base }).toFunctor.map f.fiber ≫
      (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber ≫
        (G.map f.base.op.toLoc).toFunctor.map ((α.app { as := op b.base }).toFunctor.map g.fiber) ≫
          (G.map f.base.op.toLoc).toFunctor.map ((α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber) ≫
            (G.mapComp g.base.op.toLoc f.base.op.toLoc).inv.toNatTrans.app
              ((α.app { as := op c.base }).toFunctor.obj c.fiber)
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
G : C ⟶ typeToCat.obj X
⊢ (TypeCat.homEquiv.trans
          ((ConnectedComponents.typeToCatHomEquiv (↑C) X).trans (Functor.equivCatHom (↑C) (Discrete X)))).symm
      G =
    connectedComponents.map G ≫
      { app := fun X ↦ ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X)) (𝟙 typeToCat.obj X).toFunctor,
            naturality := ⋯ }.app
        X

Tactic:
ext cc
      obtain ⟨_, _⟩ := Quotient.exists_rep cc
      cat_disch

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : (f a).get h₂ = Sum.inl b✝
h₃ : b ∈ Part.some b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
simp only [Part.mem_some_iff] at h₃; subst b; exact Or.inl ⟨h₂, e⟩

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inr ⟨a', ha', h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾f ≫ ↾g = 𝟙 X

Tactic:
ext x
      apply (h1 _ _).mp
      use f x, (hg _).2, (hf _).2

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel

Tactic:
refine
    le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
    le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_
    <;> simp [← Subobject.pullback_comp]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
⊢ φ₁ = φ₂

Tactic:
let adj := mapPullbackAdj g
  let U : Over Z := Over.mk (φ₁ ≫ snd f g)
  let φ₁' : U ⟶ (pullback g).obj (Over.mk f) := Over.homMk φ₁
  let φ₂' : U ⟶ (pullback g).obj (Over.mk f) := Over.homMk φ₂ (by simpa using! h₂.symm)
  have : φ₁' = φ₂' := by
    apply (adj.homEquiv U _).symm.injective
    apply (Over.forget X).map_injective
    simpa using! h₁
  exact congr_arg CommaMorphism.left this

Goal state after:
Module: Mathlib.CategoryTheory.DinatTrans

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ C ⥤ D
δ : F ⤞ G
α : G ⟶ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (α.app (op X✝)).app X✝ ≫ (H.obj (op X✝)).map f =
    (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (G.obj (op X✝)).map f ≫ (α.app (op X✝)).app Y✝

Tactic:
NatTrans.naturality

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ C ⥤ D
δ : F ⤞ G
α : G ⟶ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (α.app (op X✝)).app X✝ ≫ (H.obj (op X✝)).map f =
    (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (α.app (op X✝)).app X✝ ≫ (H.obj (op X✝)).map f
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := (Subobject.pullback (prod.map π₁ π₁ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le f)
      rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this
      convert! this using 3 <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ X₂ Y₂ : LocalizedMonoidal L W ε} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ₘ g = f ▷ X₂ ≫ Y₁ ◁ g

Tactic:
intros; simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
intros; simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X Y : LocalizedMonoidal L W ε} (f : X ⟶ Y), 𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
intros; simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ map p f' φ' H' φ'' ≫ map p f φ H φ' = map p f φ ⋯ φ''

Tactic:
by
  apply map_uniq p f φ
  simp only [assoc, fac]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : p.IsPreFibered
a : 𝒳
R S : 𝒮
ha : p.obj a = S
f : R ⟶ S
⊢ ∃ b φ, p.IsCartesian f φ

Tactic:
by
  subst ha; exact IsPreFibered.exists_isCartesian' f

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app i ≫ F₁.map (G.map f)) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app j) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (F₁'.map f ≫ e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app j)

Tactic:
NatTrans.naturality

Goal state after:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app i ≫ F₁.map (G.map f)) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app j) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app i ≫ (G ⋙ F₁).map f) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app j)
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
X : C
inst✝ : F.HasPointwiseLeftDerivedFunctorAt W X
⊢ L.HasPointwiseRightKanExtensionAt F (L.obj X)

Tactic:
rwa [← hasPointwiseLeftDerivedFunctorAt_iff F L W]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁)) = α.app X₁

Tactic:
adj.left_triangle_components,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ α.app X₁ ≫ L₂.map (𝟙 (G.obj X₁)) = α.app X₁