mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v b : ↥S
hb : b ∈ S.attach
hb₁ : b ≠ v
⊢ Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) b ≫ Sigma.ι f (↑b).as = 0

Tactic:
rw [Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁), zero_comp]

Goal state after:
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 : ℕ
⊢ HomologicalComplex.quasiIso C (ComplexShape.up ℤ) R.ι'

Tactic:
rw [HomologicalComplex.mem_quasiIso_iff]; infer_instance

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
Z : C
n : ℕ
⊢ {
      X₁ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) 0).X₁,
      X₂ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1)).X₁,
      X₃ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1 + 1)).X₁,
      f :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) 0).f,
      g :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1)).f,
      zero := ⋯ }.Exact

Tactic:
| =>

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ {
      X₁ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) 0).X₁,
      X₂ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1)).X₁,
      X₃ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1 + 1)).X₁,
      f :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) 0).f,
      g :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (0 + 1)).f,
      zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ n : ℕ
⊢ {
      X₁ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).X₁,
      X₂ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1)).X₁,
      X₃ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1 + 1)).X₁,
      f :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).f,
      g :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1)).f,
      zero := ⋯ }.Exact

Tactic:
| =>

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ n : ℕ
⊢ {
      X₁ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).X₁,
      X₂ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1)).X₁,
      X₃ :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1 + 1)).X₁,
      f :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).f,
      g :=
        (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
            (d (d (Injective.ι Z))) ⋯ (fun S ↦ ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1 + 1)).f,
      zero := ⋯ }.Exact
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
p : ℕ
hp : p + 1 = n
x✝ : ∃ g, g ≫ R.cocomplex.d p n = f
g : X ⟶ R.cocomplex.X p
hg : g ≫ R.cocomplex.d p n = f
⊢ (g ≫ (R.cochainComplexXIso (↑p) p ⋯).inv) ≫
      (R.cochainComplexXIso (↑p) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n) n ⋯).inv =
    f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv

Tactic:
by simp [← hg]

Goal state after:
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 : ℕ
α : Ext X Y n
m : ℕ
hm : n + 1 = m
⊢ ∃ f, ∃ (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = α

Tactic:
obtain ⟨x, rfl⟩ := R.extEquivCohomologyClass.symm.surjective α
  obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨f, hf, rfl⟩ := Cocycle.fromSingleMk_surjective x n (by simp) m (by lia)
  exact ⟨f ≫ (R.cochainComplexXIso n n rfl).hom,
    by simpa [R.cochainComplex_d _ _ _ _ rfl rfl,
      ← cancel_mono (R.cochainComplexXIso m m rfl).inv] using hf, by simp [extMk]⟩

Goal state after:
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 : ℕ
⊢ HomologicalComplex.quasiIso C (ComplexShape.up ℤ) R.π'

Tactic:
rw [HomologicalComplex.mem_quasiIso_iff]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g ↦ app f g) x).left
b : Z ⟶ ((fun g_1 ↦ app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g ↦ app f g) x).hom = b ≫ ((fun g_1 ↦ app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 ↦ app (pullback.fst f g) g_1) (Over.mk l)).hom = a ≫ x.hom

Tactic:
Category.id_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g ↦ app f g) x).left
b : Z ⟶ ((fun g_1 ↦ app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g ↦ app f g) x).hom = b ≫ ((fun g_1 ↦ app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ ((fun g_1 ↦ app (pullback.fst f g) g_1) (Over.mk l)).hom = a ≫ x.hom
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g ↦ app f g) x).left
b : Z ⟶ ((fun g_1 ↦ app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g ↦ app f g) x).hom = b ≫ ((fun g_1 ↦ app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 ↦ app (pullback.snd f g) g_1) (Over.mk l)).hom = b ≫ y.hom

Tactic:
Category.id_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g ↦ app f g) x).left
b : Z ⟶ ((fun g_1 ↦ app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g ↦ app f g) x).hom = b ≫ ((fun g_1 ↦ app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ ((fun g_1 ↦ app (pullback.snd f g) g_1) (Over.mk l)).hom = b ≫ y.hom
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 : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
this : ∀ (W : D) (z : W ⟶ L.obj X), z ≫ L.map f = 0 → ∃ l, l ≫ L.map (kernel.ι f) = z
s : Fork (L.map f) 0
x✝¹ x✝ : s.pt ⟶ (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) L).pt
h₁ : x✝¹ ≫ Fork.ι (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) L) = s.ι
h₂ : x✝ ≫ Fork.ι (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) L) = s.ι
⊢ x✝¹ = x✝

Tactic:
by simpa [cancel_mono] using h₁.trans h₂.symm

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✝
g : Arrow C
e : L.mapArrow.obj g ≅ Arrow.mk f
this : PreservesLimit (parallelPair g.hom 0) L
⊢ HasKernel f

Tactic:
have : HasLimit (parallelPair (L.map g.hom) 0) :=
      ⟨_, (KernelFork.isLimitMapConeEquiv _ L).1
        (isLimitOfPreserves L (kernelIsKernel g.hom))⟩

Goal state after:
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✝
g : Arrow C
e : L.mapArrow.obj g ≅ Arrow.mk f
this✝ : PreservesLimit (parallelPair g.hom 0) L
this : HasLimit (parallelPair (L.map g.hom) 0)
⊢ HasKernel f
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 ((F.obj X)ᘁ ⊗ F.obj X) ≫ ε_ (F.obj X) (F.obj X)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ

Tactic:
Category.id_comp

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ ε_ (F.obj X) (F.obj X)ᘁ = ε_ (F.obj X) (F.obj 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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G✝ : D ⥤ E
G : D ⥤ₑ E
⊢ exactFunctor C E (((exactFunctor D E).ι ⋙ (Functor.whiskeringLeft C D E).obj L).obj G)

Tactic:
dsimp
      simpa only [exactFunctor_comp_iff L P] using G.property

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: case refine_1
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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this✝ : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
⊢ s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z

Tactic:
s.condition_assoc,

Goal state after:
case refine_1
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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this✝ : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
⊢ s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
⊢ ∀ (g : Y ⟶ Y') (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y' X) (h_1 ≫ g) =
      (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) h_1 ≫ R.map g

Tactic:
g

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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
⊢ ∀ (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y' X) (h_1 ≫ g) =
      (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) h_1 ≫ R.map g
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)
X Y : C
Y' : B
⊢ ∀ (f : X ⟶ Y) (g : L.obj Y ⟶ Y'),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y').symm (L.map f ≫ g) =
      f ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h Y Y').symm g

Tactic:
g

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)
X Y : C
Y' : B
g : X ⟶ Y
⊢ ∀ (g_1 : L.obj Y ⟶ Y'),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y').symm (L.map g ≫ g_1) =
      g ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h Y Y').symm g_1
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ Epi q.leftTriple.rightToLeft ↔ Mono q.rightTriple.leftToRight

Tactic:
by
  rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]
  exact q.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝⁵ : L.Full
inst✝⁴ : L.Faithful
inst✝³ : G.Full
inst✝² : G.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ Epi q.leftTriple.leftToRight ↔ Mono q.rightTriple.rightToLeft

Tactic:
rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]
  exact q.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f : a ⟶ b
⊢ ∀ {Y : a ⟶ b} (f_1 : f ⟶ Y),
    (𝟭 (a ⟶ b)).map f_1 ≫ ((λ_ Y).symm ≪≫ normalizeIso nil Y).hom =
      ((λ_ f).symm ≪≫ normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map f_1

Tactic:
g

Goal state after:
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
⊢ ∀ (f_1 : f ⟶ g),
    (𝟭 (a ⟶ b)).map f_1 ≫ ((λ_ g).symm ≪≫ normalizeIso nil g).hom =
      ((λ_ f).symm ≪≫ normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map f_1
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
f : a ⟶ b
⊢ ∀ {g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
g

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
⊢ ∀ {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ
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 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:
g

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 : b ⟶ c
⊢ ∀ {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
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a✝¹ a : B
t : a ⟶ a
inst✝ : Comonad t
a✝ b✝ c✝ d✝ : LocallyDiscrete (Discrete Unit)
x✝² : a✝ ⟶ b✝
x✝¹ : b✝ ⟶ c✝
x✝ : c✝ ⟶ d✝
⊢ 𝟙 t ≫ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom

Tactic:
Category.id_comp

Goal state after:
B : Type u
inst✝¹ : Bicategory B
a✝¹ a : B
t : a ⟶ a
inst✝ : Comonad t
a✝ b✝ c✝ d✝ : LocallyDiscrete (Discrete Unit)
x✝² : a✝ ⟶ b✝
x✝¹ : b✝ ⟶ c✝
x✝ : c✝ ⟶ d✝
⊢ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ 𝟙 (F.map f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
Category.id_comp

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ 𝟙 (F.map f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
Category.id_comp

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
⊢ ∀ {X Y : (i : I) × C i} (f : X ⟶ Y),
    q.map f ≫
        (match Y with
          | ⟨i, X⟩ => (h i).app X).hom =
      (match X with
          | ⟨i, X⟩ => (h i).app X).hom ≫
        (desc F).map f

Tactic:
by
    rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
    apply (h i).hom.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ j' = k'

Tactic:
rw [← hX, ← hY, Quotient.eq'']

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ (Zigzag.setoid J) X Y
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : γ →. δ
g : β →. γ
h : α →. β
x✝¹ : α
x✝ : δ
⊢ x✝ ∈ (f.comp g).comp h x✝¹ ↔ x✝ ∈ f.comp (g.comp h) x✝¹

Tactic:
by simp only [comp_apply, Part.bind_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case x
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (homDiagram
        ((hom
            (limit.lift (F ⋙ objects)
              { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
          X✝)
        ((hom
            (limit.lift (F ⋙ objects)
              { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
          Y✝)).obj
    j

Tactic:
refine eqToHom ?_ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ?_

Goal state after:
case x.refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (hom (limit.π (F ⋙ objects) j))
      ((hom
          (limit.lift (F ⋙ objects)
            { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
        X✝) =
    (s.π.app j).toFunctor.obj X✝

case x.refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (s.π.app j).toFunctor.obj Y✝ =
    (hom (limit.π (F ⋙ objects) j))
      ((hom
          (limit.lift (F ⋙ objects)
            { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
        Y✝)
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ▷ X ≫ (∂R X Y Z).inv = coprod.inr

Tactic:
apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp
  rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_rightDistrib_hom]

Goal state after: