mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
⊢ fromIncl (asSigma f).fst (asSigma f).snd = f

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
x✝ : ((incl C).obj X).I
⊢ (fromIncl (asSigma f).fst (asSigma f).snd).f x✝ = f.f x✝

case h₂
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
i✝ : ((incl C).obj X).I
⊢ (fromIncl (asSigma f).fst (asSigma f).snd).φ i✝ ≫ eqToHom ⋯ = f.φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
⊢ (fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p) = p

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝¹ : 𝒜
x✝ : (f x✝¹).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
          x✝¹).f
      x✝ =
    (p x✝¹).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝ : 𝒜
i✝ : (f x✝).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
            x✝).φ
        i✝ ≫
      eqToHom ⋯ =
    (p x✝).φ i✝
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a
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
hh : m + 1 ≤ 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

Tactic:
induction hh using Nat.leRec with
      | refl => simp
      | @le_succ_of_le n hh ih =>
        have : homOfLE (Nat.le_succ_of_le hh) = homOfLE hh ≫ homOfLE (Nat.le_succ n) := by simp
        rw [this, op_comp, Functor.map_comp]
        simp only [Nat.succ_eq_add_one, homOfLE_leOfHom,
          Functor.ofOpSequence_map_homOfLE_succ, Category.assoc]
        have h₁ : (if _ : m < m + 1 then M m else N m) = if _ : m < n then M m else N m := by
          rw [dif_pos (by lia), dif_pos (by lia)]
        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)]
        rw [← eqToHom_trans h₁ h₂]
        slice_lhs 2 4 => rw [ih (by lia)]
        simp only [functorMap, dite_eq_ite, Pi.π, Pi.map_π_assoc]
        split_ifs
        rw [dif_pos (by lia)]
        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)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ coendRel F ⟨j, x⟩ ⟨j', x'⟩ ↔ ∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x'

Tactic:
constructor

Goal state after:
case mp
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ coendRel F ⟨j, x⟩ ⟨j', x'⟩ → ∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x'

case mpr
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ (∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x') → coendRel F ⟨j, x⟩ ⟨j', x'⟩
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 j' : J
f : j ⟶ j'
⊢ (F.map f.op).app j ≫ ι F j = (F.obj (op j')).map f ≫ ι F j'

Tactic:
ext

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
x✝ : (F.obj (op j')).obj j
⊢ (hom ((F.map f.op).app j ≫ ι F j)).toFun x✝ = (hom ((F.obj (op j')).map f ≫ ι F j')).toFun x✝
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ᵒᵖ
inst✝ : Small.{w, u'} J
⊢ ObjectProperty.preservesLimit F = (MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal

Tactic:
ext

Goal state after:
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ᵒᵖ
inst✝ : Small.{w, u'} J
x✝ : Cᵒᵖ ⥤ Type w
⊢ ObjectProperty.preservesLimit F x✝ ↔ (MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal x✝
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: case e'_2
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ᵒᵖ
inst✝ : Small.{w, u'} J
x✝ : Cᵒᵖ ⥤ Type w
hF : HasLimit F
⊢ MorphismProperty.ofHoms (preservesLimitHomFamily F) =
    MorphismProperty.single
      (coconePtToShrinkYoneda (limit.cone F) (colimit.isColimit (F.leftOp ⋙ shrinkYoneda.{w, v, u})))

Tactic:
ext

Goal state after:
case e'_2
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ᵒᵖ
inst✝ : Small.{w, u'} J
x✝ : Cᵒᵖ ⥤ Type w
hF : HasLimit F
X✝ Y✝ : Cᵒᵖ ⥤ Type w
f✝ : X✝ ⟶ Y✝
⊢ MorphismProperty.ofHoms (preservesLimitHomFamily F) f✝ ↔
    MorphismProperty.single
      (coconePtToShrinkYoneda (limit.cone F) (colimit.isColimit (F.leftOp ⋙ shrinkYoneda.{w, v, u}))) f✝
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₂
this✝¹ : W₁.IsMultiplicative
this✝ : Nonempty (Φ.RightResolution X₂)
this : IsPreconnected (Φ.RightResolution X₂)
⊢ IsConnected (Φ.RightResolution X₂)

Tactic:
constructor

Goal state after:
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:
ext

Goal state after:
case h₁
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
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝) (π₁ F G), snd := whiskerRight (𝟙 X✝) (π₂ F G), w := ⋯ }.fst.app x✝ =
    (𝟙
            { 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 }).fst.app
      x✝

case h₂
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
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝) (π₁ F G), snd := whiskerRight (𝟙 X✝) (π₂ F G), w := ⋯ }.snd.app x✝ =
    (𝟙
            { 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 }).snd.app
      x✝
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✝ 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 := ⋯ }

Tactic:
ext

Goal state after:
case h₁
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✝
x✝ : X
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ }.fst.app x✝ =
    ({ fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
            { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }).fst.app
      x✝

case h₂
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✝
x✝ : X
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ }.snd.app x✝ =
    ({ fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
            { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }).snd.app
      x✝
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✝ : 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 := ⋯ }

Tactic:
ext

Goal state after:
case hₗ
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
x✝ : X
⊢ ({ app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).fst =
    ((𝟙
            { 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 := ⋯ }).app
        x✝).fst

case hᵣ
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
x✝ : X
⊢ ({ app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).snd =
    ((𝟙
            { 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 := ⋯ }).app
        x✝).snd
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✝ 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 := ⋯ }

Tactic:
ext

Goal state after:
case hₗ
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✝
x✝ : X
⊢ ({ app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).fst =
    (({ 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 := ⋯ }).app
        x✝).fst

case hᵣ
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✝
x✝ : X
⊢ ({ app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).snd =
    (({ 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 := ⋯ }).app
        x✝).snd
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✝ Y✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (X ⥤ F ⊡ G)).map f✝ ≫
      (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).snd) ⋯)
          ⋯).hom =
    (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).snd) ⋯)
          ⋯).hom ≫
      (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f✝

Tactic:
ext

Goal state after:
case hₗ
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✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
x✝ : X
⊢ (((𝟭 (X ⥤ F ⊡ G)).map f✝ ≫
            (NatIso.ofComponents
                (fun x ↦
                  mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).snd)
                    ⋯)
                ⋯).hom).app
        x✝).fst =
    (((NatIso.ofComponents
                (fun x ↦
                  mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).snd)
                    ⋯)
                ⋯).hom ≫
            (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f✝).app
        x✝).fst

case hᵣ
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✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
x✝ : X
⊢ (((𝟭 (X ⥤ F ⊡ G)).map f✝ ≫
            (NatIso.ofComponents
                (fun x ↦
                  mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).snd)
                    ⋯)
                ⋯).hom).app
        x✝).snd =
    (((NatIso.ofComponents
                (fun x ↦
                  mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).snd)
                    ⋯)
                ⋯).hom ≫
            (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f✝).app
        x✝).snd
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✝ : CatCommSqOver F G X
⊢ whiskerRight
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj x))
            ⋯).hom
        F ≫
      ((𝟭 (CatCommSqOver F G X)).obj x✝).iso.hom =
    ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).iso.hom ≫
      whiskerRight
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj x))
            ⋯).hom
        G

Tactic:
ext

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
x✝ : X
⊢ (whiskerRight
            (NatIso.ofComponents
                (fun x ↦
                  Iso.refl
                    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).fst.obj x))
                ⋯).hom
            F ≫
          ((𝟭 (CatCommSqOver F G X)).obj x✝¹).iso.hom).app
      x✝ =
    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).iso.hom ≫
          whiskerRight
            (NatIso.ofComponents
                (fun x ↦
                  Iso.refl
                    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).snd.obj x))
                ⋯).hom
            G).app
      x✝
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝¹ x✝ : X
f : x✝¹ ⟶ x✝
⊢ J.map f ≫ (mkIso (e₁.app x✝) (e₂.app x✝) ⋯).hom = (mkIso (e₁.app x✝¹) (e₂.app x✝¹) ⋯).hom ≫ K.map f

Tactic:
ext

Goal state after:
case hₗ
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝¹ x✝ : X
f : x✝¹ ⟶ x✝
⊢ (J.map f ≫ (mkIso (e₁.app x✝) (e₂.app x✝) ⋯).hom).fst = ((mkIso (e₁.app x✝¹) (e₂.app x✝¹) ⋯).hom ≫ K.map f).fst

case hᵣ
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝¹ x✝ : X
f : x✝¹ ⟶ x✝
⊢ (J.map f ≫ (mkIso (e₁.app x✝) (e₂.app x✝) ⋯).hom).snd = ((mkIso (e₁.app x✝¹) (e₂.app x✝¹) ⋯).hom ≫ K.map f).snd
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
⊢ (toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh) = CatCommSqOver.mkIso e₁ e₂ ⋯

Tactic:
ext

Goal state after:
case h₁
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh)).hom.fst.app x✝ = (CatCommSqOver.mkIso e₁ e₂ ⋯).hom.fst.app x✝

case h₂
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh)).hom.snd.app x✝ = (CatCommSqOver.mkIso e₁ e₂ ⋯).hom.snd.app x✝