mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case inl
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : P x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩

pp: case inr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : Q x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩

Tactic:
<;>

Goal state after:
case inl
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : P x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩

case inr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : Q x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ (fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)) ≤ P

Tactic:
intro X hX

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
X : C
hX : X ∈ Set.range (Subtype.val ∘ φ)
⊢ P X
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ P ≤ isoClosure fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)

Tactic:
intro X hX

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
X : C
hX : P X
⊢ isoClosure (fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)) X
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h.left
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i) = 𝟙 X

pp: case h.right
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i = 𝟙 Y

Tactic:
<;>

Goal state after:
case h.left
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i) = 𝟙 X

case h.right
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i = 𝟙 Y
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h.left
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ Hom.hom (homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i)) = Hom.hom (𝟙 X)

pp: case h.right
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ Hom.hom (homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i) = Hom.hom (𝟙 Y)

Tactic:
<;>

Goal state after:
case h.left
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ Hom.hom (homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i)) = Hom.hom (𝟙 X)

case h.right
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ Hom.hom (homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i) = Hom.hom (𝟙 Y)
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁴ : Category.{v_2, u_2} B
T : Type u_3
inst✝³ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝² : Q.IsMultiplicative
inst✝¹ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.hom (inv f) = inv (Hom.hom f)

Tactic:
by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← comp_hom, IsIso.hom_inv_id, id_hom]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₁
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

pp: case h₂
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

case h₂
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ eqToHom ⋯ ≫ f.fiber = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).fiber

pp: case e_a.w_base
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ f.base = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).base

Tactic:
<;>

Goal state after:
case w_fiber
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ eqToHom ⋯ ≫ f.fiber = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).fiber

case e_a.w_base
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ f.base = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).base
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ (comp X✝.id f).base = f.base

pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ eqToHom ⋯ ≫ (comp X✝.id f).fiber = f.fiber

Tactic:
<;>

Goal state after:
case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ (comp X✝.id f).base = f.base

case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ eqToHom ⋯ ≫ (comp X✝.id f).fiber = f.fiber
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: case e_a.e_a.e_6
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ f = ((Grothendieck.ιNatTrans f).app X.fiber).base ≫ ((Grothendieck.ι F Y.base).map g).base

pp: case e_a.e_a.e_7
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ g ≍
    eqToHom ⋯ ≫
      (F.map ((Grothendieck.ι F Y.base).map g).base).toFunctor.map ((Grothendieck.ιNatTrans f).app X.fiber).fiber ≫
        ((Grothendieck.ι F Y.base).map g).fiber

Tactic:
<;>

Goal state after:
case e_a.e_a.e_6
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ f = ((Grothendieck.ιNatTrans f).app X.fiber).base ≫ ((Grothendieck.ι F Y.base).map g).base

case e_a.e_a.e_7
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ g ≍
    eqToHom ⋯ ≫
      (F.map ((Grothendieck.ι F Y.base).map g).base).toFunctor.map ((Grothendieck.ιNatTrans f).app X.fiber).fiber ≫
        ((Grothendieck.ι F Y.base).map g).fiber
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ : Cat
f✝ : a✝¹ ⟶ b✝
a✝ : ↑a✝¹
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app (of a✝) =
    (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app (of a✝)

pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app star =
    (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app star

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ : Cat
f✝ : a✝¹ ⟶ b✝
a✝ : ↑a✝¹
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app (of a✝) =
    (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app (of a✝)

case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app star =
    (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app star
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ : Cat
f✝ g✝ h✝ : a✝¹ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
a✝ : ↑a✝¹
⊢ (NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans)).toNatTrans.app (of a✝) =
    (NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)).toNatTrans.app (of a✝)

pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
⊢ (NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans)).toNatTrans.app star =
    (NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)).toNatTrans.app star

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ : Cat
f✝ g✝ h✝ : a✝¹ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
a✝ : ↑a✝¹
⊢ (NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans)).toNatTrans.app (of a✝) =
    (NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)).toNatTrans.app (of a✝)

case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
⊢ (NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans)).toNatTrans.app star =
    (NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)).toNatTrans.app star
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ eqToHom ⋯ ≫ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber }.fiber =
    (𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }).fiber

pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber }.base =
    (𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }).base

Tactic:
<;>

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ eqToHom ⋯ ≫ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber }.fiber =
    (𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }).fiber

case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber }.base =
    (𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }).base
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber }.fiber =
    ({ base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫
        { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }).fiber

pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber }.base =
    ({ base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫
        { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }).base

Tactic:
<;>

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber }.fiber =
    ({ base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫
        { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }).fiber

case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber }.base =
    ({ base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫
        { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }).base
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G H : D ⥤ C
α : G ≅ H
X✝ Y✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
⊢ ((pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom).base =
    (({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f).base

pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G H : D ⥤ C
α : G ≅ H
X✝ Y✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫
      ((pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom).fiber =
    (({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f).fiber

Tactic:
<;>

Goal state after:
case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G H : D ⥤ C
α : G ≅ H
X✝ Y✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
⊢ ((pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom).base =
    (({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f).base

case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G H : D ⥤ C
α : G ≅ H
X✝ Y✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫
      ((pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom).fiber =
    (({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f).fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
X : Grothendieck (G.functor ⋙ F)
⊢ ((pre F G.functor).map
          (eqToHom ⋯ ≫
            ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                    (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                X ≫
              (𝟙
                    (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                      pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).base =
    (𝟙 ((pre F G.functor).obj X)).base

pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
X : Grothendieck (G.functor ⋙ F)
⊢ eqToHom ⋯ ≫
      ((pre F G.functor).map
            (eqToHom ⋯ ≫
              ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                      (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                  X ≫
                (𝟙
                      (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                        pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                  X) ≫
          (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).fiber =
    (𝟙 ((pre F G.functor).obj X)).fiber

Tactic:
<;>

Goal state after:
case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
X : Grothendieck (G.functor ⋙ F)
⊢ ((pre F G.functor).map
          (eqToHom ⋯ ≫
            ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                    (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                X ≫
              (𝟙
                    (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                      pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).base =
    (𝟙 ((pre F G.functor).obj X)).base

case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
X : Grothendieck (G.functor ⋙ F)
⊢ eqToHom ⋯ ≫
      ((pre F G.functor).map
            (eqToHom ⋯ ≫
              ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                      (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                  X ≫
                (𝟙
                      (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                        pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                  X) ≫
          (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).fiber =
    (𝟙 ((pre F G.functor).obj X)).fiber