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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
φ : F ⟶ G
p q : F.Elements
x✝ : p ⟶ q
f : p.fst ⟶ q.fst
h : (ConcreteCategory.hom (F.map f)) p.snd = q.snd
hb :
  (ConcreteCategory.hom (φ.app q.fst)) ((ConcreteCategory.hom (F.map f)) p.snd) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (φ.app p.fst)) p.snd)
⊢ (ConcreteCategory.hom (G.map f))
      (match p with
        | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd =
    (match q with
      | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
φ : F ⟶ G
p q : F.Elements
x✝ : p ⟶ q
f : p.fst ⟶ q.fst
h : (ConcreteCategory.hom (F.map f)) p.snd = q.snd
hb :
  (ConcreteCategory.hom (φ.app q.fst)) ((ConcreteCategory.hom (F.map f)) p.snd) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (φ.app p.fst)) p.snd)
⊢ (ConcreteCategory.hom (G.map f))
      (match p with
        | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd =
    (match q with
      | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : F.Elements
f : X ⟶ Y
x✝ : PUnit.{w + 1}
⊢ (ConcreteCategory.hom ((StructuredArrow.mk (↾fun x ↦ X.snd)).hom ≫ F.map ↑f)).toFun x✝ =
    (ConcreteCategory.hom (StructuredArrow.mk (↾fun x ↦ Y.snd)).hom).toFun x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : F.Elements
f : X ⟶ Y
x✝ : PUnit.{w + 1}
⊢ (ConcreteCategory.hom ((StructuredArrow.mk (↾fun x ↦ X.snd)).hom ≫ F.map ↑f)).toFun x✝ =
    (ConcreteCategory.hom (StructuredArrow.mk (↾fun x ↦ Y.snd)).hom).toFun x✝
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ Y✝ : StructuredArrow PUnit.{w + 1} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f))) ((ConcreteCategory.hom X✝.hom) PUnit.unit) =
    (ConcreteCategory.hom (X✝.hom ≫ F.map (StructuredArrow.Hom.right f))) PUnit.unit

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ Y✝ : StructuredArrow PUnit.{w + 1} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f))) ((ConcreteCategory.hom X✝.hom) PUnit.unit) =
    (ConcreteCategory.hom (X✝.hom ≫ F.map (StructuredArrow.Hom.right f))) PUnit.unit
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f))) ((ConcreteCategory.hom X.hom) PUnit.unit) =
    (ConcreteCategory.hom (X.hom ≫ F.map (StructuredArrow.Hom.right f))) PUnit.unit

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f))) ((ConcreteCategory.hom X.hom) PUnit.unit) =
    (ConcreteCategory.hom (X.hom ≫ F.map (StructuredArrow.Hom.right f))) PUnit.unit
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (𝟙 (F.obj (unop X).1))) (unop X).snd = (unop X).snd

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (𝟙 (F.obj (unop X).1))) (unop X).snd = (unop X).snd
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ ↑((𝟭 F.Elementsᵒᵖ).map (op f) ≫
          (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst)
                ⋯).op.hom).unop =
    ↑((isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
          (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)).unop

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ ↑((𝟭 F.Elementsᵒᵖ).map (op f) ≫
          (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst)
                ⋯).op.hom).unop =
    ↑((isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
          (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)).unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯)

Tactic:
;

Goal state after:
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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (r : R),
    (algebraMap R (MvPolynomial (Fin n) A)) r ∈
      (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
intro r

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
r : R
⊢ (algebraMap R (MvPolynomial (Fin n) A)) r ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ ∀ (j : ↑(F.obj c₁)),
    colimit.ι (Grothendieck.ι F c₁ ⋙ X✝) j ≫
        (fiberwiseColimit X✝).map f ≫ colim.map ((Grothendieck.ι F c₂).whiskerLeft α) =
      colimit.ι (Grothendieck.ι F c₁ ⋙ X✝) j ≫
        colim.map ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y✝).map f

Tactic:
;

Goal state after:
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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ ∀ (j : ↑(F.obj c₁)),
    colimit.ι (Grothendieck.ι F c₁ ⋙ X✝) j ≫
        (fiberwiseColimit X✝).map f ≫ colim.map ((Grothendieck.ι F c₂).whiskerLeft α) =
      colimit.ι (Grothendieck.ι F c₁ ⋙ X✝) j ≫
        colim.map ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y✝).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ }.app x✝ =
    (𝟙 (fiberwiseColimit G)).app x✝

Tactic:
;

Goal state after:
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✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ }.app x✝ =
    (𝟙 (fiberwiseColimit G)).app x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
x✝ : C
⊢ colimMap (𝟙 (Grothendieck.ι F x✝ ⋙ G)) = 𝟙 (colimit (Grothendieck.ι F x✝ ⋙ G))

Tactic:
;

Goal state after:
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✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
x✝ : C
⊢ colimMap (𝟙 (Grothendieck.ι F x✝ ⋙ G)) = 𝟙 (colimit (Grothendieck.ι F x✝ ⋙ G))
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ }.app x✝ =
    ({ app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ } ≫
          { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ }).app
      x✝

Tactic:
;

Goal state after:
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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ }.app x✝ =
    ({ app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ } ≫
          { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ }).app
      x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
x✝ : C
⊢ colimMap ((Grothendieck.ι F x✝).whiskerLeft α ≫ (Grothendieck.ι F x✝).whiskerLeft β) =
    colimMap ((Grothendieck.ι F x✝).whiskerLeft α) ≫ colimMap ((Grothendieck.ι F x✝).whiskerLeft β)

Tactic:
;

Goal state after:
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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
x✝ : C
⊢ colimMap ((Grothendieck.ι F x✝).whiskerLeft α ≫ (Grothendieck.ι F x✝).whiskerLeft β) =
    colimMap ((Grothendieck.ι F x✝).whiskerLeft α) ≫ colimMap ((Grothendieck.ι F x✝).whiskerLeft β)
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base✝, fiber := fiber✝ }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base✝, fiber := fiber✝ }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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 G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (colimMap (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x✝) G).hom) ≫
        colimit.pre (Grothendieck.ι F x✝ ⋙ G) (F.map f).toFunctor) ≫
      colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ 𝟙 c.pt

Tactic:
;

Goal state after:
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 G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (colimMap (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x✝) G).hom) ≫
        colimit.pre (Grothendieck.ι F x✝ ⋙ G) (F.map f).toFunctor) ≫
      colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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 G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
j✝ : ↑(F.obj x✝¹)
⊢ colimit.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x✝) G).hom) ≫
          colimit.pre (Grothendieck.ι F x✝ ⋙ G) (F.map f).toFunctor) ≫
        colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ 𝟙 c.pt

Tactic:
;

Goal state after:
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 G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
j✝ : ↑(F.obj x✝¹)
⊢ colimit.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x✝) G).hom) ≫
          colimit.pre (Grothendieck.ι F x✝ ⋙ G) (F.map f).toFunctor) ≫
        colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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 G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
⊢ colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c✝) ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    s.ι.app c

Tactic:
;

Goal state after:
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 G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
⊢ colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c✝) ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    s.ι.app c
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: 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 G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
j✝ : ↑(F.obj c)
⊢ colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c✝) ≫
        hc.desc
          { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫ s.ι.app c

Tactic:
;

Goal state after:
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 G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
j✝ : ↑(F.obj c)
⊢ colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c✝) ≫
        hc.desc
          { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫ s.ι.app c
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: 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 ⟶ Y
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber

Tactic:
;

Goal state after:
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 ⟶ Y
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).base = eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).base = eqToHom ⋯
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯).base).toFunctor.obj X.fiber = X.fiber

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯).base).toFunctor.obj X.fiber = X.fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).fiber = eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).fiber = eqToHom ⋯
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ X.base = X.base

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ X.base = X.base
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = X.fiber

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = X.fiber
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝ : HasColimitsOfShape C H
X✝ Y✝ : Grothendieck F ⥤ H
x✝ : X✝ ⟶ Y✝
⊢ ∀ (j : C),
    colimit.ι ((fiberwiseColim F H).obj X✝) j ≫
        (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
      colimit.ι ((fiberwiseColim F H).obj X✝) j ≫ (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝ : HasColimitsOfShape C H
X✝ Y✝ : Grothendieck F ⥤ H
x✝ : X✝ ⟶ Y✝
⊢ ∀ (j : C),
    colimit.ι ((fiberwiseColim F H).obj X✝) j ≫
        (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
      colimit.ι ((fiberwiseColim F H).obj X✝) j ≫ (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝