mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝² : EnrichedOrdinaryCategory V C
F₁ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₁
⊢ (functorHomEquiv V) (𝟙 F₁) = functorEnrichedId V F₁

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ S.ShortExact

Tactic:
have : Mono S.f := by
      rw [hP.jointlyReflectMonomorphisms.mono_iff]
      exact fun i ↦ (hS i).mono_f

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
this : Mono S.f
⊢ S.ShortExact
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
α : Type u_4
c : ComplexShape α
K L : HomologicalComplex C c
f : K ⟶ L
⊢ QuasiIso f ↔ ∀ (i : I), QuasiIso (((F i).mapHomologicalComplex c).map f)

Tactic:
simp only [_root_.quasiIso_iff, hP.quasiIsoAt_iff]
  tauto

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ Nonempty (IsInitial X) ↔ IsEmpty (F.obj X).obj

Tactic:
rw [(IsInitial.isInitialIffObj F X).nonempty_congr]
  exact Concrete.initial_iff_empty_of_preserves_of_reflects (F.obj X)

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

Goal state before:
pp: G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
⊢ IsIso i.hom

Tactic:
refine (ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩

Goal state after:
case refine_1
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
⊢ Function.Injective ⇑(ConcreteCategory.hom i.hom)

case refine_2
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.FintypeCat.ofMulAction G X).V.obj
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
⊢ WalkingPair.casesOn WalkingPair.right c₁.pt c₂.pt ⟶ s.pt

Tactic:
exact Cofan.IsColimit.desc h₂ (fun a ↦ s.inj (.inr a))

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
x✝ : ∃ y, (autEmbedding F) y = a
i : Arrow C
σ : Aut F
h : (autEmbedding F) σ = a
⊢ F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F✝ : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F✝
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : ContAction FintypeCat (Aut F)
this : ContinuousSMul (Aut F) X.obj.V.obj
A : C
i : (functorToAction F).obj A ≅ X.obj
⊢ (functorToContAction F).essImage X

Tactic:
exact ⟨A, ⟨ObjectProperty.isoMk _ i⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous
    ((fun p ↦ X.obj.V.uSwitchEquiv.symm p) ∘
      (fun p ↦ (ConcreteCategory.hom (X.obj.ρ p.1).hom) p.2) ∘ fun p ↦ (p.1, X.obj.V.uSwitchEquiv p.2))

Tactic:
exact Continuous.comp (by fun_prop) (Continuous.comp X.2.1 (by fun_prop))

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
V : Type u_1
inst✝¹ : Quiver V
inst✝ : Nonempty V
⊢ Nonempty (Quiver.FreeGroupoid V)

Tactic:
by
  inhabit V; exact ⟨⟨@default V _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
x✝ : op (left a✝¹) ⟶ op (left a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (left a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (left a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
x✝ : op (right a✝¹) ⟶ op (left a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (left a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (right a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
x✝ : op (right a✝¹) ⟶ op (right a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (right a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (right a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝ : C
⊢ (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.map
        ((NatIso.ofComponents
                (fun x ↦
                  match x with
                  | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
                  | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a))))
                ⋯).hom.app
          (op (left a✝))) ≫
      (NatIso.ofComponents
              (fun x ↦
                match x with
                | left a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (left a))
                | right a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (right a)))
              ⋯).hom.app
        ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp.obj
          (op (left a✝))) =
    𝟙
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.obj
        (op (left a✝)))

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝ : D
⊢ (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.map
        ((NatIso.ofComponents
                (fun x ↦
                  match x with
                  | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
                  | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a))))
                ⋯).hom.app
          (op (right a✝))) ≫
      (NatIso.ofComponents
              (fun x ↦
                match x with
                | left a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (left a))
                | right a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (right a)))
              ⋯).hom.app
        ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp.obj
          (op (right a✝))) =
    𝟙
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.obj
        (op (right a✝)))

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
⊢ map (𝟙 F) = 𝟙 (chosenCoend F)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ lift f hf ≫ π F j = f j

Tactic:
by
  apply IsLimit.fac

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
⊢ map (𝟙 F) = 𝟙 (chosenEnd F)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : (c₁.map (F.flip.obj Y₂)).pt ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
l' : (c₂.map (F.obj c₁.pt)).pt ⟶ s.pt
hl' : Cofork.π (c₂.map (F.obj c₁.pt)) ≫ l' = l
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l' = Cofork.π s

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
f : Y ⟶ h.pullback
f_p₁ : f ≫ h.p₁ = g₁
f_p₂ : f ≫ h.p₂ = g₂
f_p✝¹ : f ≫ h.p = b
f' : Y ⟶ h.pullback
f'_p₁ : f' ≫ h.p₁ = g₁
f'_p₂ : f' ≫ h.p₂ = g₂
f_p✝ : f' ≫ h.p = b
⊢ f = f'

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
⊢ g₁ ≫ f₁ = g₂ ≫ f₂

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
⊢ g₂ ≫ f₂ = g₃ ≫ f₃

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
⊢ φ₁₂ ≫ h₁₂.p₂ = φ₂₃ ≫ h₂₃.p₁

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₂.pullback
b : x✝ ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
φ : x✝ ⟶ h.pullback
hφ₁ : φ ≫ h.p₁ = a ≫ h₁₂.p₁
hφ₂ : φ ≫ h.p₂ = a ≫ h₁₂.p₂
hφ₃ : φ ≫ h.p₃ = b ≫ h₁₃.p₂
⊢ φ ≫ h.p₁₂ = a

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₂.pullback
b : x✝ ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
φ : x✝ ⟶ h.pullback
hφ₁ : φ ≫ h.p₁ = a ≫ h₁₂.p₁
hφ₂ : φ ≫ h.p₂ = a ≫ h₁₂.p₂
hφ₃ : φ ≫ h.p₃ = b ≫ h₁₃.p₂
⊢ φ ≫ h.p₁₃ = b

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
φ : x✝ ⟶ h.pullback
hφ₁ : φ ≫ h.p₁ = a ≫ h₁₃.p₁
hφ₂ : φ ≫ h.p₂ = b ≫ h₂₃.p₁
hφ₃ : φ ≫ h.p₃ = a ≫ h₁₃.p₂
⊢ φ ≫ h.p₁₃ = a

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
φ : x✝ ⟶ h.pullback
hφ₁ : φ ≫ h.p₁ = a ≫ h₁₃.p₁
hφ₂ : φ ≫ h.p₂ = b ≫ h₂₃.p₁
hφ₃ : φ ≫ h.p₃ = a ≫ h₁₃.p₂
⊢ φ ≫ h.p₂₃ = b

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
X : Type (max w u)
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
x : chosenCoend F
x✝¹ x✝ : (j : J) × (F.obj (op j)).obj j
h : Types.coendRel F x✝¹ x✝
⊢ (hom (f x✝¹.fst)) x✝¹.snd = (hom (f x✝.fst)) x✝.snd

Tactic:
cases h with | mk f x => exact ConcreteCategory.congr_hom (hf f) _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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 : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
⊢ (CatCommSq.iso F (ψ.comp φ).left (ψ.comp φ).base F'').hom ≫
      Functor.whiskerRight (Functor.whiskerRight α.left φ.left) F'' =
    F.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫ (CatCommSq.iso F (ψ'.comp φ).left (ψ'.comp φ).base F'').hom

Tactic:
ext x
    dsimp
    simp only [CatCommSq.vComp_iso_hom_app, Category.assoc]
    rw [← Functor.map_comp_assoc, ← left_coherence_app, Functor.map_comp_assoc]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
u : ↑(F ⋙ P).sections
⊢ (fun f ↦ ⟨fun j ↦ shrinkYonedaEquiv (c'.ι.app (op j) ≫ f), ⋯⟩)
      ((fun s ↦ hc'.desc { pt := P, ι := { app := fun j ↦ shrinkYonedaEquiv.symm (↑s (unop j)), naturality := ⋯ } })
        u) =
    u

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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 : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
⊢ ψ ◁ θ ≫ η ▷ φ' = η ▷ φ ≫ ψ' ◁ θ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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 : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
⊢ 𝟙 ψ ▷ φ = 𝟙 (ψ.comp φ)

Tactic:
by cat_disch

Goal state after: