mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

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:
;

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:
;

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:
;

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:
;

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.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:
exact congr($(mapWhiskerRight_rightUnitor_hom D _).toCatHom₂)

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✝
x✝ : FormalCoproduct C
⊢ { app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom (x✝² ≫ x✝¹).unop), naturality := ⋯ }.app x✝ =
    ({ app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom x✝².unop), naturality := ⋯ } ≫
          { app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom x✝¹.unop), naturality := ⋯ }).app
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X✝ Y✝ Z✝ : Type tᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : FormalCoproduct C
⊢ { app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom (x✝² ≫ x✝¹).unop), naturality := ⋯ }.app x✝ =
    ({ app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom x✝².unop), naturality := ⋯ } ≫
          { app := fun x ↦ x.mapPower ⇑(ConcreteCategory.hom x✝¹.unop), naturality := ⋯ }).app
      x✝
Module: Mathlib.CategoryTheory.Limits.Pi

Goal state before:
pp: I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
⊢ (fun i ↦ (P i).lift (coneCompEval s i)) ≫ (coneOfConeCompEval c).π.app j = s.π.app j

Tactic:
by
    funext i
    exact (P i).fac (coneCompEval s i) j

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
X✝ Y✝ Z✝ : FormalCoproduct C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
n✝ : SimplexCategoryᵒᵖ
⊢ { app := fun x ↦ powerMap (x✝¹ ≫ x✝) (ToType (Opposite.unop x)), naturality := ⋯ }.app n✝ =
    ({ app := fun x ↦ powerMap x✝¹ (ToType (Opposite.unop x)), naturality := ⋯ } ≫
          { app := fun x ↦ powerMap x✝ (ToType (Opposite.unop x)), naturality := ⋯ }).app
      n✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
X✝ Y✝ Z✝ : FormalCoproduct C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
n✝ : SimplexCategoryᵒᵖ
⊢ { app := fun x ↦ powerMap (x✝¹ ≫ x✝) (ToType (Opposite.unop x)), naturality := ⋯ }.app n✝ =
    ({ app := fun x ↦ powerMap x✝¹ (ToType (Opposite.unop x)), naturality := ⋯ } ≫
          { app := fun x ↦ powerMap x✝ (ToType (Opposite.unop x)), naturality := ⋯ }).app
      n✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f : X.I → Y.I
F G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = { f := f, φ := G }.φ i
i : X.I
⊢ F i = G i

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f : X.I → Y.I
F G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = { f := f, φ := G }.φ i
i : X.I
⊢ F i = G i
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ L.map (factorThruImage f) ≫ L.map (image.ι f) = L.map f

Tactic:
← L.map_comp,

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ L.map (factorThruImage f ≫ image.ι f) = L.map f
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case e'_3
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) = ↑((homPullbackEquiv f g pb hpb s.pt).1 m)

Tactic:
;

Goal state after:
case e'_3
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) = ↑((homPullbackEquiv f g pb hpb s.pt).1 m)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq 0 0 biprod.inl biprod.inr

Tactic:
convert! of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)

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

Goal state before:
pp: case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : m < n + 1
⊢ M m = M m

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
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m

Tactic:
;

Goal state after:
case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : m < n + 1
⊢ M m = M m

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
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m
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
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m

Tactic:
;

Goal state after:
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
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_2
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ M m = M m

Tactic:
;

Goal state after:
case refine_2
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ M m = M m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:

Tactic:
;

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

Goal state before:
pp: case refine_3
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = N m

Tactic:
;

Goal state after:
case refine_3
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = N m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_4
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ N m = N m

Tactic:
;

Goal state after:
case refine_4
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ N m = N m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
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 n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
⊢ functorMap f n ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
have h₂ : (if _ : m < n then M m else N m) = if _ : m < n + 1 then M m else N m := by
          rw [dif_pos h, dif_pos (by lia)]

Goal state after:
case e_a.le_succ_of_le
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 n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ functorMap f n ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: 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), HasProductsOfShape (a ⟶ b) D
X Y : Under F
e : X ≅ Y
⊢ Coequifibered X.hom → Coequifibered X.hom

Tactic:
;

Goal state after:
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), HasProductsOfShape (a ⟶ b) D
X Y : Under F
e : X ≅ Y
⊢ Coequifibered X.hom → Coequifibered X.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
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 n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
| @le_succ_of_le n hh ih =>

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:
;

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: case mk
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend J)), (cowedge F).ι.app j ≫ m = s.ι.app j
x✝ : (cowedge F).pt
j : (j : J) × (F.obj (op j)).obj j
⊢ (hom m).toFun (Quot.mk (coendRel F) j) =
    (hom (↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯)).toFun (Quot.mk (coendRel F) j)

Tactic:
;

Goal state after:
case mk
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend J)), (cowedge F).ι.app j ≫ m = s.ι.app j
x✝ : (cowedge F).pt
j : (j : J) × (F.obj (op j)).obj j
⊢ (hom m).toFun (Quot.mk (coendRel F) j) =
    (hom (↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯)).toFun (Quot.mk (coendRel F) j)
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁷ : Category.{v_1, u_5} K
inst✝⁶ : Category.{v_2, u_6} K'
inst✝⁵ : Category.{v_3, u_1} J
inst✝⁴ : Category.{v_4, u_2} J'
inst✝³ : Category.{v_5, u_3} C
inst✝² : Category.{v_6, u_4} D
inst✝¹ : HasColimitsOfShape K' C
inst✝ : HasExactColimitsOfShape K' C
⊢ preservesFiniteLimits.colimitsOfShape K' ≤ preservesFiniteLimits

Tactic:
by
    rintro G ⟨h⟩
    have := h.prop_diag_obj
    exact ⟨fun K _ _ ↦ (preservesLimitsOfShape K).prop_of_isColimit h.isColimit inferInstance⟩

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

Goal state before:
pp: case refine_2
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j✝ j'✝ : J
g : j✝ ⟶ j'✝
y : (F.obj (op j'✝)).obj j✝
⊢ (hom ((G.obj (op j'✝)).map g)) ((hom ((f.app (op j'✝)).app j✝)) y) =
    (hom ((f.app (op j'✝)).app j'✝)) ((Hom.hom ((F.obj (op j'✝)).map g)) y)

Tactic:
· simp [← NatTrans.naturality_apply]

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)
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:
;

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.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
K : Type u_2
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F✝ : J ⥤ C
D : Type u_4
inst✝¹ : Category.{v_4, u_4} D
G : K ⥤ D
F : J ⥤ C
inst✝ : HasWeakLimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
;

Goal state after:
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
K : Type u_2
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F✝ : J ⥤ C
D : Type u_4
inst✝¹ : Category.{v_4, u_4} D
G : K ⥤ D
F : J ⥤ C
inst✝ : HasWeakLimit F
j : J
⊢ F.obj j = F.obj j
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

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₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
X₂ : C₂
⊢ (W₂.inverseImage Φ.functor).IsMultiplicative

Tactic:
;

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₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
X₂ : C₂
⊢ (W₂.inverseImage Φ.functor).IsMultiplicative
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

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₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
⊢ (W₂.inverseImage Φ.functor).IsMultiplicative

Tactic:
;

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₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
⊢ (W₂.inverseImage Φ.functor).IsMultiplicative
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✝ : 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 }

Tactic:
;

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 }