mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_9
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsTerminal.from X

pp: case e'_10
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsTerminal.from Y

Tactic:
<;>

Goal state after:
case e'_9
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsTerminal.from X

case e'_10
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsTerminal.from Y
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_4✝ : X = (pair X Y).obj { as := WalkingPair.left }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.left })

pp: case e'_8
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_5✝ : Y = (pair X Y).obj { as := WalkingPair.right }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.right })

Tactic:
<;>

Goal state after:
case e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_4✝ : X = (pair X Y).obj { as := WalkingPair.left }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.left })

case e'_8
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_5✝ : Y = (pair X Y).obj { as := WalkingPair.right }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.right })
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_7
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to X

pp: case e'_8
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to Y

Tactic:
<;>

Goal state after:
case e'_7
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to X

case e'_8
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to Y
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
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 0 b.inl b.inr

Tactic:
convert! IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
    <;> subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ 2 ^ α ≤ #(X ⟶ yp)

pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(X ⟶ yp) ≤ α

Tactic:
· apply le_trans (Cardinal.power_le_power_right z)
      rw [Cardinal.power_def]
      apply le_of_eq
      rw [Cardinal.eq]
      refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
      · intro f
        ext k
        simp [yp]
      · intro f
        ext ⟨j⟩
        simp [yp]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(X ⟶ yp) ≤ α
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 ⋯) ≫
      Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m

Tactic:
simp only [dite_eq_ite, limit.lift_π_assoc,
        Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc]

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
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if m < n then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case left
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
a✝ : (multispanShapeCoend J).L
⊢ (cowedge F).ι.app (WalkingMultispan.left a✝) ≫ ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯ =
    s.ι.app (WalkingMultispan.left a✝)

pp: case right
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
a✝ : (multispanShapeCoend J).R
⊢ (cowedge F).ι.app (WalkingMultispan.right a✝) ≫ ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯ =
    s.ι.app (WalkingMultispan.right a✝)

Tactic:
<;>

Goal state after:
case left
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
a✝ : (multispanShapeCoend J).L
⊢ (cowedge F).ι.app (WalkingMultispan.left a✝) ≫ ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯ =
    s.ι.app (WalkingMultispan.left a✝)

case right
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
a✝ : (multispanShapeCoend J).R
⊢ (cowedge F).ι.app (WalkingMultispan.right a✝) ≫ ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯ =
    s.ι.app (WalkingMultispan.right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: case left
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.left = θ'.left

pp: case right
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.right = θ'.right

pp: case base
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.base = θ'.base

Tactic:
<;>

Goal state after:
case left
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.left = θ'.left

case right
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.right = θ'.right

case base
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.base = θ'.base
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case left
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)
s : Cone (multicospanIndexEnd F).multicospan
a✝ : (multicospanShapeEnd J).L
⊢ (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩) ≫ (wedge F).π.app (WalkingMulticospan.left a✝) =
    s.π.app (WalkingMulticospan.left a✝)

pp: case right
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)
s : Cone (multicospanIndexEnd F).multicospan
a✝ : (multicospanShapeEnd J).R
⊢ (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩) ≫ (wedge F).π.app (WalkingMulticospan.right a✝) =
    s.π.app (WalkingMulticospan.right a✝)

Tactic:
<;>

Goal state after:
case left
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)
s : Cone (multicospanIndexEnd F).multicospan
a✝ : (multicospanShapeEnd J).L
⊢ (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩) ≫ (wedge F).π.app (WalkingMulticospan.left a✝) =
    s.π.app (WalkingMulticospan.left a✝)

case right
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)
s : Cone (multicospanIndexEnd F).multicospan
a✝ : (multicospanShapeEnd J).R
⊢ (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩) ≫ (wedge F).π.app (WalkingMulticospan.right a✝) =
    s.π.app (WalkingMulticospan.right a✝)
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'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ f.left ≫ (inv f).left = 𝟙 ψ'.left ∧ (inv f).left ≫ f.left = 𝟙 ψ'.left

Tactic:
by simp [← CatCospanTransform.category_comp_left]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_1.isMin
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
hj : IsMin ⊥
⊢ hf.incl.app ⊥ ≫ g₁ = hf.incl.app ⊥ ≫ g₂

Tactic:
simpa [← cancel_epi hf.isoBot.inv]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
refine ⟨fun g₁ g₂ h ↦ hf.isColimit.hom_ext (fun j ↦ ?_), fun g ↦ ?_⟩
    · dsimp at h ⊢
      induction j using SuccOrder.limitRecOn with
      | isMin j hj =>
        obtain rfl := hj.eq_bot
        simpa [← cancel_epi hf.isoBot.inv]
      | succ j hj hj' => exact (hf.map_mem j hj _ hZ).1 (by simpa)
      | isSuccLimit j hj hj' =>
        exact (hf.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
          (fun ⟨k, hk⟩ ↦ by simpa using! hj' _ hk)
    · let d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData :=
        .ofExists (fun j hj ↦ (hf.map_mem j hj _ hZ).2) (fun j hj s ↦ by
          let c : Cocone ((Set.principalSegIio j).monotone.functor ⋙ hf.F) :=
            { pt := Z
              ι.app k := s.1 (op k)
              ι.naturality _ _ g := by
                dsimp
                simpa only [Category.comp_id] using! s.2 g.op }
          exact ⟨(hf.F.isColimitOfIsWellOrderContinuous j hj).desc c, fun k hk ↦
            by simpa using! (hf.F.isColimitOfIsWellOrderContinuous j hj).fac c ⟨k, hk⟩⟩)
      let σ := d.sectionsMk (hf.isoBot.hom ≫ g)
      let c : Cocone hf.F :=
        { pt := Z
          ι.app j := σ.1 (op j)
          ι.naturality _ _ f := by
            dsimp
            simpa only [Category.comp_id] using! σ.2 f.op }
      exact ⟨hf.isColimit.desc c, by
        simp only [← hf.fac, Category.assoc, hf.isColimit.fac c ⊥, c, σ,
          d.sectionsMk_val_op_bot, Iso.inv_hom_id_assoc]⟩

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

Goal state before:
pp: case fst
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 y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.fst = g.fst

pp: case snd
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 y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.snd = g.snd

Tactic:
<;>

Goal state after:
case fst
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 y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.fst = g.fst

case snd
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 y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.snd = g.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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✝

pp: 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✝

Tactic:
<;>

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

pp: 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✝

Tactic:
<;>

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

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

Tactic:
<;>

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