mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : Y ⟶ A
k₂ : Z ⟶ A
hk : f ≫ k₁ = 0 ∧ k₁ = g ≫ k₂
⊢ (f ≫ g) ≫ biprod.inr ≫ (biprod.fst ≫ k₁ + biprod.snd ≫ k₂) = 0

Tactic:
obtain ⟨hk, rfl⟩ := hk

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₂ : Z ⟶ A
hk : f ≫ g ≫ k₂ = 0
⊢ (f ≫ g) ≫ biprod.inr ≫ (biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂) = 0
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : Y ⟶ A
k₂ : Z ⟶ A
hk✝ : φ f g ≫ (biprod.fst ≫ k₁ + biprod.snd ≫ k₂) = 0
hk : f ≫ k₁ = 0 ∧ k₁ = g ≫ k₂
⊢ π f g ≫ cokernel.desc (f ≫ g) (biprod.inr ≫ (biprod.fst ≫ k₁ + biprod.snd ≫ k₂)) ⋯ = biprod.fst ≫ k₁ + biprod.snd ≫ k₂

Tactic:
obtain ⟨hk, rfl⟩ := hk

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₂ : Z ⟶ A
hk✝ : φ f g ≫ (biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂) = 0
hk : f ≫ g ≫ k₂ = 0
⊢ π f g ≫ cokernel.desc (f ≫ g) (biprod.inr ≫ (biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂)) ⋯ =
    biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (generator F)

Tactic:
rw [generator]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective (∐ fun X ↦ ∐ fun x ↦ projectiveSeparator C)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
⊢ ∑ x ∈ F.attach,
      h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun a ↦ G) x ≫ (ModuleCat.Hom.hom f) (↑x).as =
    0

Tactic:
let r (x : F) : (End G)ᵐᵒᵖ := MulOpposite.op (h ≫ pullback.fst _ _ ≫ Sigma.π _ x)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ ∑ x ∈ F.attach,
      h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun a ↦ G) x ≫ (ModuleCat.Hom.hom f) (↑x).as =
    0
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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
⊢ L.map f ≫ L.map g = 0 ↔ P Z

Tactic:
rw [← L.map_comp, map_eq_zero_iff L P]

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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
⊢ P (Abelian.image (f ≫ g)) ↔ P Z
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
⊢ (MorphismProperty.epimorphisms D).inverseImage L = P.epiModSerre

Tactic:
ext
  simp [epi_map_iff L P]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ (beckAlgebraCofork X).π ≫ { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ } = s.π

Tactic:
ext
      simpa [← T.η.naturality_assoc, T.left_unit_assoc] using! T.η.app ((T : C ⥤ C).obj X.A) ≫= h₁

Goal state after:
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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (R.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction U)).symm))
this : (X : (monadicAdjunction U).toMonad.Algebra) → RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X) :=
  fun X ↦
    ⋯.mpr
      { W := (monadicAdjunction U).toMonad.free.obj ((monadicAdjunction U).toMonad.obj X.A),
        left := Monad.FreeCoequalizer.topMap X, right := Monad.FreeCoequalizer.bottomMap X, w := ⋯,
        isColimit := Monad.beckAlgebraCoequalizer X }
⊢ R'.IsRightAdjoint

Tactic:
exact isRightAdjoint_triangle_lift R' (Monad.adj _) this

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv

Tactic:
rw [θ.naturality_id]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a

Tactic:
rw [θ.naturality_id]
      bicategory

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a a' : α
hb : b ∈ f.fix a
ha' : Sum.inr a' ∈ f a
⊢ b ∈ f.fix a'

Tactic:
by rwa [← fix_fwd_eq ha']

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
Y : C
⊢ ((tensorBifunctor L W ε).map ε.inv).app (L'.obj Y) ≫
      (μ L W ε (𝟙_ C) Y).hom ≫ L'.map (λ_ Y).hom ≫ 𝟙 (L'.obj Y) ≫ 𝟙 (L'.obj Y) =
    ((tensorBifunctor L W ε).map (ε' L W ε).inv).app (L'.obj Y) ≫ (μ L W ε (𝟙_ C) Y).hom ≫ L'.map (λ_ Y).hom

Tactic:
simp only [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C
f g : x ⟶ y
⊢ (Sum.inl_ C C').map f = (Sum.inl_ C C').map g

Tactic:
((by assumption : IsDiscrete C).subsingleton x y).allEq f g

Goal state after:
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C
f g : x ⟶ y
⊢ (Sum.inl_ C C').map g = (Sum.inl_ C C').map g
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 : C
⊢ ((tensorBifunctor L W ε).obj (L'.obj X)).map ε.inv ≫
      (μ L W ε X (𝟙_ C)).hom ≫ L'.map (ρ_ X).hom ≫ 𝟙 (L'.obj X) ≫ 𝟙 (L'.obj X) =
    ((tensorBifunctor L W ε).obj (L'.obj X)).map (ε' L W ε).inv ≫ (μ L W ε X (𝟙_ C)).hom ≫ L'.map (ρ_ X).hom

Tactic:
simp only [comp_id]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ ((X.tensorObjImpl Y).tensorObjImpl Z).rel =
    (Subobject.pullback (prod.map (prod.associator X.src Y.src Z.src).hom (prod.associator X.tgt Y.tgt Z.tgt).hom)).obj
      (X.tensorObjImpl (Y.tensorObjImpl Z)).rel

Tactic:
by
    simp [Subobject.inf_pullback, ← Subobject.pullback_comp, inf_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : C ≌ D
x✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ≌ D)).map x✝ ≫ (Iso.refl ((𝟭 (C ≌ D)).obj Y✝)).hom =
    (Iso.refl ((𝟭 (C ≌ D)).obj X✝)).hom ≫ (symmEquivFunctor C D ⋙ symmEquivInverse C D).map x✝

Tactic:
ext c

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : C ≌ D
x✝ : X✝ ⟶ Y✝
c : C
⊢ (asNatTrans ((𝟭 (C ≌ D)).map x✝ ≫ (Iso.refl ((𝟭 (C ≌ D)).obj Y✝)).hom)).app c =
    (asNatTrans ((Iso.refl ((𝟭 (C ≌ D)).obj X✝)).hom ≫ (symmEquivFunctor C D ⋙ symmEquivInverse C D).map x✝)).app c
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
hRS : R = S
a : 𝒳
ha : p.obj a = R
⊢ p.IsHomLift (eqToHom hRS) (𝟙 a)

Tactic:
subst hRS ha

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 a)
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
simpa using (fac 𝒳.p f φ)

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

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := ⋯
inv_hom : φ' ≫ φ = 𝟙 b
h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
⊢ (φ ≫ φ') ≫ φ = 𝟙 a ≫ φ

Tactic:
simp only [assoc, inv_hom, comp_id, id_comp]

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 φ
inst✝ : IsIso f
⊢ IsIso φ

Tactic:
subst_hom_lift p f φ; clear a b R S
  -- Let `φ` be the morphism induced by applying universal property to `𝟙 b` lying over `f⁻¹ ≫ f`.
  let φ' := map p (p.map φ) φ (IsIso.inv_hom_id (p.map φ)).symm (𝟙 b)
  use φ'
  -- `φ' ≫ φ = 𝟙 b` follows immediately from the universal property.
  have inv_hom : φ' ≫ φ = 𝟙 b := fac p (p.map φ) φ _ (𝟙 b)
  refine ⟨?_, inv_hom⟩
  -- We will now show that `φ ≫ φ' = 𝟙 a` by showing that `(φ ≫ φ') ≫ φ = 𝟙 a ≫ φ`.
  have h₁ : IsHomLift p (𝟙 (p.obj a)) (φ ≫ φ') := by
    rw [← IsIso.hom_inv_id (p.map φ)]
    apply IsHomLift.comp
  apply IsStronglyCartesian.ext p (p.map φ) φ (𝟙 (p.obj a))
  simp only [assoc, inv_hom, comp_id, id_comp]

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.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
let ψ := pullbackMap (domain_eq p f φ) g

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

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.IsCocartesian f φ
b' : 𝒳
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift (𝟙 S) ψ
inst✝ : p.IsHomLift (𝟙 S) ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ IsCocartesian.map p f φ (φ ≫ ψ) = ψ'

Tactic:
map_uniq p f φ (φ ≫ ψ) ψ' h.symm

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsCocartesian f φ
b' : 𝒳
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift (𝟙 S) ψ
inst✝ : p.IsHomLift (𝟙 S) ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ IsCocartesian.map p f φ (φ ≫ ψ) = IsCocartesian.map p f φ (φ ≫ ψ)
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b✝ = φ

Tactic:
simp only [comp_id]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝² : HasFibers p
R S : 𝒮
a : 𝒳
b b' : Fib p R
f : R ⟶ S
ψ : (ι R).obj b' ⟶ a
inst✝¹ : p.IsCartesian f ψ
φ : (ι R).obj b ⟶ a
inst✝ : p.IsHomLift f φ
⊢ (ι R).map (inducedMap f ψ φ) ≫ ψ = φ

Tactic:
simp only [inducedMap, Fib.map_homMk, IsCartesian.fac]

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

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.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst✝ : p.IsHomLift f' φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
subst_hom_lift p f' φ'; clear a b R S
  have : p.IsHomLift (f ≫ g) φ' := (hf' ▸ inferInstance)
  apply IsStronglyCocartesian.universal_property' f

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b✝ = φ

Tactic:
simp only [comp_id]

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

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ' ≫ φ = 𝟙 b

Tactic:
apply IsStronglyCocartesian.ext p (p.map φ) φ (𝟙 (p.obj b))

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := ⋯
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ ≫ φ' ≫ φ = φ ≫ 𝟙 b
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
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
m : s.pt ⟶ (coneFunctorEnrichedHom V F₁ F₂).pt
hm : ∀ (j : J), m ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j
⊢ m = lift s

Tactic:
by
    dsimp
    ext j
    simpa using ((hm j).trans (fac s j).symm) =≫ enrichedHomπ V _ _ (Under.mk (𝟙 j))

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

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
⊢ (fiberInclusion.obj Y).base = S

Tactic:
simpa using! Y.2

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
⊢ IsColimit (cocone F)

Tactic:
refine evaluationJointlyReflectsColimits _ (fun X ↦ ?_)

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
⊢ IsColimit (((evaluation C (Type u₂)).obj X).mapCocone (cocone F))
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
⊢ (∃ (h : c = d), f = eqToHom h) → f ∈ discrete.arrows c d

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
C : Type u
inst✝ : Groupoid C
c : C
⊢ eqToHom ⋯ ∈ discrete.arrows c c
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ HasBiproduct F

Tactic:
apply hasBiproduct_of_total (Biproducts.bicone F)
          simpa using! biproduct.map_eq.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X✝ Y✝ Z✝ : Type tᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom (x✝¹ ≫ x✝).unop), naturality := ⋯ } =
    { app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom x✝¹.unop), naturality := ⋯ } ≫
      { app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom x✝.unop), naturality := ⋯ }

Tactic:
ext : 2; simp [types_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.FiniteProducts

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
J : Type
inst✝³ : HasProductsOfShape J C
inst✝² : W.IsStableUnderProductsOfShape J
inst✝¹ : W.ContainsIdentities
inst✝ : Finite J
F : Discrete J ⥤ C
⊢ (adj L W J).counit.app (F ⋙ L) =
    (const (Discrete J)).map ((compLimitFunctorIso L W J).hom.app F) ≫
      (compConstIso (Discrete J) L).hom.app (lim.obj F) ≫ whiskerRight (constLimAdj.counit.app F) L

Tactic:
by
  apply constLimAdj.localization_counit_app

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

Goal state before:
pp: C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
t : X ⟶ Y
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
⊢ motive t

Tactic:
induction t using Quotient.inductionOn with | _ f
  induction f with
  | id X => exact id X
  | α_hom X Y Z => exact α_hom X Y Z
  | α_inv X Y Z => exact α_inv X Y Z
  | l_hom X => exact l_hom X
  | l_inv X => exact l_inv X
  | ρ_hom X => exact ρ_hom X
  | ρ_inv X => exact ρ_inv X
  | comp f g hf hg => exact comp _ _ hf hg
  | whiskerLeft X f hf => exact whiskerLeft X _ hf
  | whiskerRight f X hf => exact whiskerRight _ X hf
  | @tensor W X Y Z f g hf hg =>
      have : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g :=
        Quotient.sound (HomEquiv.tensorHom_def f g)
      change motive (homMk f ⊗ₘ homMk g)
      rw [this]
      exact comp _ _ (whiskerRight _ _ hf) (whiskerLeft _ _ hg)

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ (pullbackPushforwardAdj (f ≫ g)).unit ≫ (pullback (f ≫ g)).whiskerLeft (pushforwardComp f g).hom =
    (pullbackPushforwardAdj (f ≫ g)).unit

Tactic:
pushforwardComp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ (pullbackPushforwardAdj (f ≫ g)).unit ≫
      (pullback (f ≫ g)).whiskerLeft
        ((pullbackPushforwardAdj (f ≫ g)).rightAdjointUniq (pullbackPushforwardAdj (f ≫ g))).hom =
    (pullbackPushforwardAdj (f ≫ g)).unit
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ Functor.whiskerRight (pushforwardComp f g).hom (pullback (f ≫ g)) ≫ (pullbackPushforwardAdj (f ≫ g)).counit =
    (pullbackPushforwardAdj (f ≫ g)).counit

Tactic:
pushforwardComp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ Functor.whiskerRight ((pullbackPushforwardAdj (f ≫ g)).rightAdjointUniq (pullbackPushforwardAdj (f ≫ g))).hom
        (pullback (f ≫ g)) ≫
      (pullbackPushforwardAdj (f ≫ g)).counit =
    (pullbackPushforwardAdj (f ≫ g)).counit