mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d e : C} {p : c ⟶ d}, p ∈ univ → ∀ {q : d ⟶ e}, q ∈ univ → p ≫ q ∈ univ

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ univ
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ univ
⊢ p✝ ≫ q✝ ∈ univ
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
⊢ ∀ {c d e : C} {p : c ⟶ d},
    p ∈ {f | φ.map f ∈ S.arrows (φ.obj c) (φ.obj d)} →
      ∀ {q : d ⟶ e},
        q ∈ {f | φ.map f ∈ S.arrows (φ.obj d) (φ.obj e)} → p ≫ q ∈ {f | φ.map f ∈ S.arrows (φ.obj c) (φ.obj e)}

Tactic:
intros

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ p✝ ≫ q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj e✝)}
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p, inl := P.decompId_i,
            inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.fst ≫
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inl +
      { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.snd ≫
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inr =
    𝟙
      { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
          inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
          inr_snd := ⋯ }.pt

Tactic:
by
      ext
      simp only [complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, add_def, idem,
        comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel, id_f]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c : Cat} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (f ◁ η).toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)).hom ≫
        (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ≫
          (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)).inv

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
a✝ b✝ c✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ h✝
⊢ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (f✝ ◁ η✝).toNatTrans) =
    (Cat.Hom.isoMk (mapCompRight C f✝.toFunctor g✝.toFunctor)).hom ≫
      (mapPair (𝟭 C) f✝.toFunctor).toCatHom ◁ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η✝.toNatTrans) ≫
        (Cat.Hom.isoMk (mapCompRight C f✝.toFunctor h✝.toFunctor)).inv
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η ▷ h).toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)).hom ≫
        NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ▷ (mapPair (𝟭 C) h.toFunctor).toCatHom ≫
          (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)).inv

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
a✝ b✝ c✝ : Cat
f✝ g✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
⊢ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η✝ ▷ h✝).toNatTrans) =
    (Cat.Hom.isoMk (mapCompRight C f✝.toFunctor h✝.toFunctor)).hom ≫
      NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η✝.toNatTrans) ▷ (mapPair (𝟭 C) h✝.toFunctor).toCatHom ≫
        (Cat.Hom.isoMk (mapCompRight C g✝.toFunctor h✝.toFunctor)).inv
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (α_ f g h).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C (f ≫ g).toFunctor h.toFunctor)).hom ≫
        (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)).hom ▷ (mapPair (𝟭 C) h.toFunctor).toCatHom ≫
          (α_ (mapPair (𝟭 C) f.toFunctor).toCatHom (mapPair (𝟭 C) g.toFunctor).toCatHom
                (mapPair (𝟭 C) h.toFunctor).toCatHom).hom ≫
            (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapCompRight C f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (α_ f✝ g✝ h✝).hom.toNatTrans) =
    (Cat.Hom.isoMk (mapCompRight C (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
      (Cat.Hom.isoMk (mapCompRight C f✝.toFunctor g✝.toFunctor)).hom ▷ (mapPair (𝟭 C) h✝.toFunctor).toCatHom ≫
        (α_ (mapPair (𝟭 C) f✝.toFunctor).toCatHom (mapPair (𝟭 C) g✝.toFunctor).toCatHom
              (mapPair (𝟭 C) h✝.toFunctor).toCatHom).hom ≫
          (mapPair (𝟭 C) f✝.toFunctor).toCatHom ◁ (Cat.Hom.isoMk (mapCompRight C g✝.toFunctor h✝.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapCompRight C f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (λ_ f).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C (𝟙 a).toFunctor f.toFunctor)).hom ≫
        (Cat.Hom.isoMk mapPairId).hom ▷ (mapPair (𝟭 C) f.toFunctor).toCatHom ≫
          (λ_ (mapPair (𝟭 C) f.toFunctor).toCatHom).hom

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (λ_ f✝).hom.toNatTrans) =
    (Cat.Hom.isoMk (mapCompRight C (𝟙 a✝).toFunctor f✝.toFunctor)).hom ≫
      (Cat.Hom.isoMk mapPairId).hom ▷ (mapPair (𝟭 C) f✝.toFunctor).toCatHom ≫
        (λ_ (mapPair (𝟭 C) f✝.toFunctor).toCatHom).hom
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (ρ_ f).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor (𝟙 b).toFunctor)).hom ≫
        (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
          (ρ_ (mapPair (𝟭 C) f.toFunctor).toCatHom).hom

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (ρ_ f✝).hom.toNatTrans) =
    (Cat.Hom.isoMk (mapCompRight C f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
      (mapPair (𝟭 C) f✝.toFunctor).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
        (ρ_ (mapPair (𝟭 C) f✝.toFunctor).toCatHom).hom
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c : Cat} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    NatTrans.toCatHom₂ (mapWhiskerRight (f ◁ η).toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor g.toFunctor)).hom ≫
        (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ NatTrans.toCatHom₂ (mapWhiskerRight η.toNatTrans (𝟭 D)) ≫
          (Cat.Hom.isoMk (mapCompLeft D f.toFunctor h.toFunctor)).inv

Tactic:
intros

Goal state after:
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝ b✝ c✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ h✝
⊢ NatTrans.toCatHom₂ (mapWhiskerRight (f✝ ◁ η✝).toNatTrans (𝟭 D)) =
    (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor g✝.toFunctor)).hom ≫
      (mapPair f✝.toFunctor (𝟭 D)).toCatHom ◁ NatTrans.toCatHom₂ (mapWhiskerRight η✝.toNatTrans (𝟭 D)) ≫
        (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor h✝.toFunctor)).inv
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    NatTrans.toCatHom₂ (mapWhiskerRight (η ▷ h).toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor h.toFunctor)).hom ≫
        NatTrans.toCatHom₂ (mapWhiskerRight η.toNatTrans (𝟭 D)) ▷ (mapPair h.toFunctor (𝟭 D)).toCatHom ≫
          (Cat.Hom.isoMk (mapCompLeft D g.toFunctor h.toFunctor)).inv

Tactic:
intros

Goal state after:
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝ b✝ c✝ : Cat
f✝ g✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
⊢ NatTrans.toCatHom₂ (mapWhiskerRight (η✝ ▷ h✝).toNatTrans (𝟭 D)) =
    (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor h✝.toFunctor)).hom ≫
      NatTrans.toCatHom₂ (mapWhiskerRight η✝.toNatTrans (𝟭 D)) ▷ (mapPair h✝.toFunctor (𝟭 D)).toCatHom ≫
        (Cat.Hom.isoMk (mapCompLeft D g✝.toFunctor h✝.toFunctor)).inv
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    NatTrans.toCatHom₂ (mapWhiskerRight (α_ f g h).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D (f ≫ g).toFunctor h.toFunctor)).hom ≫
        (Cat.Hom.isoMk (mapCompLeft D f.toFunctor g.toFunctor)).hom ▷ (mapPair h.toFunctor (𝟭 D)).toCatHom ≫
          (α_ (mapPair f.toFunctor (𝟭 D)).toCatHom (mapPair g.toFunctor (𝟭 D)).toCatHom
                (mapPair h.toFunctor (𝟭 D)).toCatHom).hom ≫
            (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk (mapCompLeft D g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapCompLeft D f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
intros

Goal state after:
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ NatTrans.toCatHom₂ (mapWhiskerRight (α_ f✝ g✝ h✝).hom.toNatTrans (𝟭 D)) =
    (Cat.Hom.isoMk (mapCompLeft D (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
      (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor g✝.toFunctor)).hom ▷ (mapPair h✝.toFunctor (𝟭 D)).toCatHom ≫
        (α_ (mapPair f✝.toFunctor (𝟭 D)).toCatHom (mapPair g✝.toFunctor (𝟭 D)).toCatHom
              (mapPair h✝.toFunctor (𝟭 D)).toCatHom).hom ≫
          (mapPair f✝.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk (mapCompLeft D g✝.toFunctor h✝.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerRight (λ_ f).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D (𝟙 a).toFunctor f.toFunctor)).hom ≫
        (Cat.Hom.isoMk mapPairId).hom ▷ (mapPair f.toFunctor (𝟭 D)).toCatHom ≫
          (λ_ (mapPair f.toFunctor (𝟭 D)).toCatHom).hom

Tactic:
intros

Goal state after:
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ NatTrans.toCatHom₂ (mapWhiskerRight (λ_ f✝).hom.toNatTrans (𝟭 D)) =
    (Cat.Hom.isoMk (mapCompLeft D (𝟙 a✝).toFunctor f✝.toFunctor)).hom ≫
      (Cat.Hom.isoMk mapPairId).hom ▷ (mapPair f✝.toFunctor (𝟭 D)).toCatHom ≫
        (λ_ (mapPair f✝.toFunctor (𝟭 D)).toCatHom).hom
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerRight (ρ_ f).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor (𝟙 b).toFunctor)).hom ≫
        (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
          (ρ_ (mapPair f.toFunctor (𝟭 D)).toCatHom).hom

Tactic:
intros

Goal state after:
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ NatTrans.toCatHom₂ (mapWhiskerRight (ρ_ f✝).hom.toNatTrans (𝟭 D)) =
    (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
      (mapPair f✝.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
        (ρ_ (mapPair f✝.toFunctor (𝟭 D)).toCatHom).hom
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n : ℕ
⊢ HasWidePullback ((incl C).obj T) (fun x ↦ U) fun x ↦ (isTerminalIncl T hT).from U

Tactic:
have : HasProduct fun (x : Fin (n + 1)) ↦ U := ⟨⟨_, U.isLimitPowerFan (Fin (n + 1))⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n : ℕ
this : HasProduct fun x ↦ U
⊢ HasWidePullback ((incl C).obj T) (fun x ↦ U) fun x ↦ (isTerminalIncl T hT).from U
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
this : (F.obj Y₁).map f₂ ≫ Cofork.π s = coprod.inr ≫ 0
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l

Tactic:
← dsimp% hl,

Goal state after:
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
this : (F.obj Y₁).map f₂ ≫ (F.map (Cofork.π c₁)).app Y₂ ≫ l = coprod.inr ≫ 0
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l
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
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
⊢ l ≫ h.p₁ ≫ f₁ = g₁ ≫ f₁

Tactic:
reassoc_of% h₁

Goal state after:
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
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
⊢ g₁ ≫ f₁ = g₁ ≫ f₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case refine_3
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ G.left.map f = s.fst
hm₂ : m ≫ G.hom.app i = s.snd
k : J
⊢ (m ≫ (Over.Hom.left (α.app k)).app i) ≫ (c.obj k).left.map f =
    ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯ ≫ (c.obj k).left.map f

Tactic:
simp [← NatTrans.naturality, reassoc_of% hm₁]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ ((Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
        (cone f).π.app (Opposite.op n)) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m

Tactic:
simp only [Category.assoc]
      rw [cone_π_app_comp_Pi_π_neg f _ _ h]
      simp only [dite_eq_ite, limit.lift_π_assoc,
        Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc]
      slice_lhs 2 4 => simp only [← dite_eq_ite, ← functorMap_commSq f h]
      simp

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)
⊢ ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f.op).app i ≫ coend.ι F i = (F.obj (op j)).map f ≫ coend.ι F j

Tactic:
intros

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
⊢ (F.map f✝.op).app i✝ ≫ coend.ι F i✝ = (F.obj (op j✝)).map f✝ ≫ coend.ι F j✝
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)
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
⊢ ∀ ⦃i j : J⦄ (f : i ⟶ j), end_.π F i ≫ (F.obj (op i)).map f = end_.π F j ≫ (F.map f.op).app j

Tactic:
intros

Goal state after:
J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
⊢ end_.π F i✝ ≫ (F.obj (op i✝)).map f✝ = end_.π F j✝ ≫ (F.map f✝.op).app j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ (X_1 : X ⥤ F ⊡ G),
    { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ } =
      𝟙
        { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
          iso :=
            X_1.associator (π₁ F G) F ≪≫
              X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm }

Tactic:
intros

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
⊢ { fst := whiskerRight (𝟙 X✝) (π₁ F G), snd := whiskerRight (𝟙 X✝) (π₂ F G), w := ⋯ } =
    𝟙
      { fst := X✝ ⋙ π₁ F G, snd := X✝ ⋙ π₂ F G,
        iso :=
          X✝.associator (π₁ F G) F ≪≫
            X✝.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X✝.associator (π₂ F G) G).symm }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ {X_1 Y Z : X ⥤ F ⊡ G} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { fst := whiskerRight (f ≫ g) (π₁ F G), snd := whiskerRight (f ≫ g) (π₂ F G), w := ⋯ } =
      { fst := whiskerRight f (π₁ F G), snd := whiskerRight f (π₂ F G), w := ⋯ } ≫
        { fst := whiskerRight g (π₁ F G), snd := whiskerRight g (π₂ F G), w := ⋯ }

Tactic:
intros

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ } =
    { fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
      { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ (X_1 : CatCommSqOver F G X),
    { app := fun x ↦ { fst := (𝟙 X_1).fst.app x, snd := (𝟙 X_1).snd.app x, w := ⋯ }, naturality := ⋯ } =
      𝟙
        { obj := fun x ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x },
          map := fun {x y} f ↦ { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }

Tactic:
intros

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : CatCommSqOver F G X
⊢ { app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    𝟙
      { obj := fun x ↦ { fst := X✝.fst.obj x, snd := X✝.snd.obj x, iso := X✝.iso.app x },
        map := fun {x y} f ↦ { fst := X✝.fst.map f, snd := X✝.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ {X_1 Y Z : CatCommSqOver F G X} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { app := fun x ↦ { fst := (f ≫ g).fst.app x, snd := (f ≫ g).snd.app x, w := ⋯ }, naturality := ⋯ } =
      { app := fun x ↦ { fst := f.fst.app x, snd := f.snd.app x, w := ⋯ }, naturality := ⋯ } ≫
        { app := fun x ↦ { fst := g.fst.app x, snd := g.snd.app x, w := ⋯ }, naturality := ⋯ }

Tactic:
intros

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : CatCommSqOver F G X
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    { app := fun x ↦ { fst := f✝.fst.app x, snd := f✝.snd.app x, w := ⋯ }, naturality := ⋯ } ≫
      { app := fun x ↦ { fst := g✝.fst.app x, snd := g✝.snd.app x, w := ⋯ }, naturality := ⋯ }