mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft (colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda) i)).app j ≫
                (K.whiskerLeft
                      ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                          (Presheaf.isColimitTautologicalCocone A)).hom).app
                  j

Tactic:
← NatTrans.comp_app,

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft (colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda) i) ≫
                    K.whiskerLeft
                      ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                          (Presheaf.isColimitTautologicalCocone A)).hom).app
                j
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
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
have (i : ι) : HasColimit (F i) := ⟨_, hc i⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))
Module: Mathlib.CategoryTheory.Abelian.Indization

Goal state before:
pp: C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w✝¹ : SmallCategory I
w✝ : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map ϕ)
i' : Arrow.mk (coimageImageComparison f) ≅ Arrow.mk (coimageImageComparison ((Ind.lim I).map ϕ)) :=
  coimageImageComparisonFunctor.mapIso i
this : IsIso i'.hom
⊢ IsIso (coimageImageComparison ((Ind.lim I).map ϕ))

Tactic:
Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv

Goal state after:
C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w✝¹ : SmallCategory I
w✝ : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map ϕ)
i' : Arrow.mk (coimageImageComparison f) ≅ Arrow.mk (coimageImageComparison ((Ind.lim I).map ϕ)) :=
  coimageImageComparisonFunctor.mapIso i
this : IsIso i'.hom
⊢ IsIso ((Ind.lim I).map (coimageImageComparison ϕ))
Module: Mathlib.CategoryTheory.Abelian.Indization

Goal state before:
pp: C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
⊢ IsIso (coimageImageComparison f)

Tactic:
by
  obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)
  let i' := coimageImageComparisonFunctor.mapIso i
  dsimp only [coimageImageComparisonFunctor_obj, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom] at i'
  have := Iso.isIso_hom i'
  rw [Arrow.isIso_iff_isIso_of_isIso i'.hom,
    Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
⊢ IsLimit { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }

Tactic:
by
  suffices IsIso (limMap (pushout.inr c.π ((Functor.const J).map f))) from
    Cone.isLimitOfIsIsoLimMapπ _
  have hpush := lim.map_isPushout (IsPushout.of_hasPushout c.π ((Functor.const J).map f))
  dsimp only [lim_obj, lim_map] at hpush
  have := hc.isIso_limMap_π
  apply hpush.isIso_inr_of_isIso

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ (Over.Hom.left (Φ.toColon Ψ).hom).app X ≫ (Φ.colon Ψ).ι.app X = Φ.ι.app X

Tactic:
← NatTrans.comp_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ (Over.Hom.left (Φ.toColon Ψ).hom ≫ (Φ.colon Ψ).ι).app X = Φ.ι.app X
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
⊢ IsTrans (Over P) (PseudoEqual P)

Tactic:
refine ⟨fun f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩ ↦ ?_⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
⊢ G.kernel ≤ G.kernel

Tactic:
by rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ P.isoModSerre (Abelian.factorThruImage f)

Tactic:
rw [isoModSerre_iff_of_epi]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ P.monoModSerre (Abelian.factorThruImage f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
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
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.isoModSerre (cokernel.π (f₁ - f₂))

Tactic:
rw [isoModSerre_iff_of_epi]

Goal state after:
case refine_1
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
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.monoModSerre (cokernel.π (f₁ - f₂))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
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
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.monoModSerre (cokernel.π (f₁ - f₂))

Tactic:
exact (exists_isoModSerre_comp_eq_zero_iff P _).1 ⟨_, s, hs, by simpa [sub_eq_zero]⟩

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
J : Type u_3
inst✝ : Category.{v_2, u_3} J
F : J ⥤ Action V G
c✝ : Cocone F
h : IsColimit ((forget V G).mapCocone c✝)
⊢ IsColimit c✝

Tactic:
apply isColimitOfReflects ((Action.functorCategoryEquivalence V G).functor)

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
J : Type u_3
inst✝ : Category.{v_2, u_3} J
F : J ⥤ Action V G
c✝ : Cocone F
h : IsColimit ((forget V G).mapCocone c✝)
⊢ IsColimit ((functorCategoryEquivalence V G).functor.mapCocone c✝)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing (G.obj ᘁ(F.obj X)) X

Tactic:
letI := exactPairingCongrLeft (X := F.obj (G.obj ᘁ(F.obj X)))
      (X' := ᘁ(F.obj X)) (Y := F.obj X) (adj.toEquivalence.counitIso.app ᘁ(F.obj X))
    apply ExactPairing.ofFullyFaithful F

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    Quot.map (Hom₂.whisker_left (f ≫ g)) ⋯ η =
      { hom := Quot.mk Rel (Hom₂.associator f g h), inv := Quot.mk Rel (Hom₂.associator_inv f g h), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        Quot.map (Hom₂.whisker_left f) ⋯ (Quot.map (Hom₂.whisker_left g) ⋯ η) ≫
          { hom := Quot.mk Rel (Hom₂.associator f g h'), inv := Quot.mk Rel (Hom₂.associator_inv f g h'),
              hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv

Tactic:
by
    rintro a b c d f g h h' ⟨η⟩
    exact Quot.sound (Rel.comp_whisker_left f g η)

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

Goal state before:
pp: case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (g.comp g✝)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g✝))

Tactic:
erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]

Goal state after:
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.mapComp' f (𝟙 b₁) f ⋯).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom

Tactic:
rw [mapComp']

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₂Iso (eqToIso ⋯) ≪≫ F.mapComp f (𝟙 b₁)).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).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.mapComp' (𝟙 b₀) f f ⋯).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom

Tactic:
rw [mapComp']

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₂Iso (eqToIso ⋯) ≪≫ F.mapComp (𝟙 b₀) f).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
⊢ ∀ (X Y : ↑((objects ⋙ typeToCat).obj x✝²)) (f : X ⟶ Y),
    ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
      (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f

Tactic:
intro ⟨_⟩

Goal state after:
X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
as✝ : objects.obj x✝²
⊢ ∀ (Y : ↑((objects ⋙ typeToCat).obj x✝²)) (f : { as := as✝ } ⟶ Y),
    ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
      (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
  · simp only [prodLift, Part.mem_mk_iff, And.exists, Prod.ext_iff]
  · simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
J✝ : Type v
inst✝ : Category.{v, v} J✝
F : J✝ ⥤ Cat
⊢ (limit.cone (F ⋙ objects)).pt ≅ (objects.mapCone (HasLimits.limitCone F)).pt

Tactic:
by rfl

Goal state after:
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✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ (∂L X Y Z).hom = coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr)

Tactic:
by rfl

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

Goal state before:
pp: case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F = prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F

Tactic:
rw [← Category.assoc]

Goal state after:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F = (prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F)) ≫ f₁.F
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
⊢ (∂R X Y Z).hom = coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)

Tactic:
by rfl

Goal state after:
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₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F = prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F

Tactic:
rw [← Category.assoc]

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F = (prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F)) ≫ f₂.F
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
val✝ : A
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inl val✝)) =
    𝟙
      (match inl val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)

Tactic:
(simp only [← map_id]; rfl)

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

Goal state before:
pp: case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
val✝ : B
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inr val✝)) =
    𝟙
      (match inr val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)

Tactic:
(simp only [← map_id]; rfl)

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

Goal state before:
pp: case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
      prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F)

Tactic:
ext <;> simp <;> (rw [← Category.assoc]; congr 1; simp)

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ e a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ e b

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ e b
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 ε
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
obtain ⟨X', ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩
  obtain ⟨Y', ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩
  have h₁ := (associator_hom_app L W ε X' (𝟙_ _) Y' =≫
    (𝟙 ((L').obj X') ⊗ₘ (μ L W ε (𝟙_ C) Y').hom))
  simp only [assoc, id_tensorHom, ← whiskerLeft_comp,
    Iso.inv_hom_id, whiskerLeft_id, comp_id, Iso.inv_hom_id,
    ← cancel_mono (μ L W ε X' (𝟙_ C ⊗ Y')).hom] at h₁
  have h₂ := (ε' L W ε).hom ▷ (L').obj Y' ≫= leftUnitor_hom_app L W ε Y'
  simp only [← whiskerRight_comp_assoc, Iso.hom_inv_id, whiskerRight_id, id_comp] at h₂
  have h₃ := (((μ L W ε _ _).hom ⊗ₘ 𝟙 _) ≫ (μ L W ε _ _).hom) ≫=
    ((L').congr_map (MonoidalCategory.triangle X' Y'))
  simp only [assoc, Functor.map_comp, ← reassoc_of% h₁] at h₃
  rw [← μ_natural_left, tensorHom_id, ← whiskerRight_comp_assoc,
    ← μ_natural_right, ← Iso.comp_inv_eq, assoc, assoc, assoc,
    Iso.hom_inv_id, comp_id, ← whiskerLeft_comp, ← h₂] at h₃
  replace h₃ := ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫= (h₃ =≫ (_ ◁ e₂.hom)) =≫ (e₁.hom ▷ _)
  simp only [← whiskerLeft_comp, assoc, ← leftUnitor_naturality, ← whisker_exchange] at h₃
  have : _ = (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom :=
    triangle_aux₁ _ _ _ e₁.symm ε.symm e₂.symm
  simp only [← this, Iso.symm_hom, Iso.symm_inv, assoc,
    ← id_tensorHom, ← tensor_comp, comp_id]
  convert! h₃
  · exact triangle_aux₂ _ _ _ e₁ e₂
  · exact triangle_aux₃ _ _ _ e₁ e₂

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:
by
    -- Let `ψ` be a Cartesian arrow lying over `g`
    let ψ := pullbackMap (domain_eq p f φ) g
    -- Let `τ` be the map induced by the universal property of `ψ ≫ φ`.
    let τ := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
    use τ ≫ ψ
    -- It is easily verified that `τ ≫ ψ` lifts `g` and `τ ≫ ψ ≫ φ = φ'`
    refine ⟨⟨inferInstance, by simp only [assoc, IsCartesian.fac, τ]⟩, ?_⟩
    -- It remains to check that `τ ≫ ψ` is unique.
    -- So fix another lift `π` of `g` satisfying `π ≫ φ = φ'`.
    intro π ⟨hπ, hπ_comp⟩
    -- Write `π` as `π = τ' ≫ ψ` for some `τ'` induced by the universal property of `ψ`.
    rw [← fac p g ψ π]
    -- It remains to show that `τ' = τ`. This follows again from the universal property of `ψ`.
    congr 1
    apply map_uniq
    rwa [← assoc, IsCartesian.fac]

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 i) ≫
      eHomWhiskerLeft V (F₁.obj (G.obj i)) (F₂.map (G.map f)) ≫
        eHomWhiskerLeft V (F₁.obj (G.obj i)) (e₂.hom.app j) ≫ eHomWhiskerRight V (e₁.inv.app i) (F₂'.obj j) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j) ≫ eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)

Tactic:
rw [enrichedHom_condition_assoc, eHom_whisker_exchange,
        eHom_whisker_exchange, ← eHomWhiskerRight_comp_assoc,
        ← eHomWhiskerRight_comp_assoc, 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)