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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map ((adj.homEquiv g.left d) g.hom) ≫ u.hom = g.hom

Tactic:
by

Goal state after:
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
G✝ : C ⥤ Type w
G : D ⥤ C
X✝ Y✝ Z✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := G.map (f ≫ g).base, fiber := (f ≫ g).fiber }.fiber =
    ({ base := G.map f.base, fiber := f.fiber } ≫ { base := G.map g.base, fiber := g.fiber }).fiber

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom =
      (Cat.Hom.isoMk (mapComp (𝟙 a).toFunctor f.toFunctor)).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (mapId ↑a)).hom (prelaxfunctor.map f) ≫
          (Bicategory.leftUnitor (prelaxfunctor.map f)).hom

Tactic:
by

Goal state after:
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
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 := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
      (map (whiskerRight α.hom F) ⋙ pre F H).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (d ⟶ F.obj X) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : d ⟶ F.obj X₀
z : Z X₀ k₀
⊢ Z (lift F d) (homToLift F d)

Tactic:
by

Goal state after:
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
G✝ : C ⥤ Type w
G : D ≌ C
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) ≅ pre F G.functor ⋙ preInv F G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom =
      (Cat.Hom.isoMk (mapComp f.toFunctor (𝟙 b).toFunctor)).hom ≫
        Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapId ↑b)).hom ≫
          (Bicategory.rightUnitor (prelaxfunctor.map f)).hom

Tactic:
by

Goal state after:
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
G✝ : C ⥤ Type w
G : D ≌ C
⊢ ∀ (X : Grothendieck (G.functor ⋙ F)),
    (pre F G.functor).map
          ((eqToIso ⋯ ≪≫
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).isoWhiskerLeft
                      (Grothendieck.preUnitIso F G) ≪≫
                    eqToIso ⋯).hom.app
            X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
      𝟙 ((pre F G.functor).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WithTerminal C
⊢ ∀ (a : X ⟶ star),
    a =
      match X with
      | of a => PUnit.unit
      | star => PUnit.unit

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
⊢ (F.map (𝟙 { base := c, fiber := X✝ }.base)).toFunctor.obj { base := c, fiber := X✝ }.fiber = X✝

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
d : ↑(F.obj c)
⊢ { base := 𝟙 { base := c, fiber := d }.base, fiber := eqToHom ⋯ ≫ 𝟙 d } = 𝟙 { base := c, fiber := d }

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f ≫ g }.base =
    ({ base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f } ≫
        { base := 𝟙 { base := c, fiber := Y✝ }.base, fiber := eqToHom ⋯ ≫ g }).base

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (starTerminal.from (incl.obj x)) ≫ (liftStar F M hM).hom = (inclLift F M hM).hom.app x ≫ M x

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f ≫ g } =
    { base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f } ≫
      { base := 𝟙 { base := c, fiber := Y✝ }.base, fiber := eqToHom ⋯ ≫ g }

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ : ↑(F.obj c)
a₁✝ a₂✝ : X✝ ⟶ Y✝
f : (ι F c).map a₁✝ = (ι F c).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ ({ base := 𝟙 X, fiber := eqToHom ⋯ ≫ x✝ } ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝¹) }).base =
    ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝²) } ≫
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x✝ }).base

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ eqToHom ⋯ ≫
      ({ base := 𝟙 X, fiber := eqToHom ⋯ ≫ x✝ } ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝¹) }).fiber =
    ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝²) } ≫
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x✝ }).fiber

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ (ι F X).map x✝ ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((ι F X).obj x✝¹).fiber) } =
    { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((ι F X).obj x✝²).fiber) } ≫ ((F.map f).toFunctor ⋙ ι F Y).map x✝

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
c : C
⊢ fib c = (F.map (𝟙 c)).toFunctor ⋙ fib c

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map (f ≫ g)).toFunctor ⋙ fib c₃

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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
⊢ x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map (f ≫ g)).toFunctor ⋙ fib c₃

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) =
      hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom (@_proof_146 C inst✝² F E inst✝ fib c₁ c₂ c₃ f g)
X : Grothendieck F
⊢ (hom (𝟙 X).base).app X.fiber ≫ (fib X.base).map (𝟙 X).fiber = 𝟙 ((fib X.base).obj X.fiber)

Tactic:
by

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

Goal state before:
pp: case z
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map ?k₀ ≫ c.ι.app ?X₀

Tactic:
← Functor.map_comp_assoc

Goal state after:
case z
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map (f ≫ homToLift F Y) ≫ c.ι.app (lift F Y) = G.map ?k₀ ≫ c.ι.app (lift F Y)
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) =
    (G.map (homToLift F X) ≫ c.ι.app (lift F X)) ≫ ((const D).obj c.pt).map f

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) =
      hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom (@_proof_146 C inst✝² F E inst✝ fib c₁ c₂ c₃ f g)
X✝ Y✝ Z✝ : Grothendieck F
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (hom (f ≫ g).base).app X✝.fiber ≫ (fib Z✝.base).map (f ≫ g).fiber =
    ((hom f.base).app X✝.fiber ≫ (fib Y✝.base).map f.fiber) ≫ (hom g.base).app Y✝.fiber ≫ (fib Z✝.base).map g.fiber

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) =
      hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom (@_proof_146 C inst✝² F E inst✝ fib c₁ c₂ c₃ f g)
c : C
X✝ Y✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
⊢ (ι F c ⋙ functorFrom fib (fun {c c'} ↦ hom) hom_id hom_comp).map f ≫
      (Iso.refl ((ι F c ⋙ functorFrom fib (fun {c c'} ↦ hom) hom_id hom_comp).obj Y✝)).hom =
    (Iso.refl ((ι F c ⋙ functorFrom fib (fun {c c'} ↦ hom) hom_id hom_comp).obj X✝)).hom ≫ (fib c).map f

Tactic:
by

Goal state after:
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
G : C ⥤ Type w
F' : C ⥤ Cat
α : F ⟶ F'
c : C
X✝ Y✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
⊢ (ι F c ⋙ map α).map f ≫ (Iso.refl ((ι F c ⋙ map α).obj Y✝)).hom =
    (Iso.refl ((ι F c ⋙ map α).obj X✝)).hom ≫ ((α.app c).toFunctor ⋙ ι F' c).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    G.map f ≫
        (match Y with
          | of x => h.app x
          | star => hG).hom =
      (match X with
          | of x => h.app x
          | star => hG).hom ≫
        (lift F M hM).map f

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
j x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ s.π.app x✝¹ = s.π.app x✝

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
j : J
⊢ s.π.app (Classical.arbitrary J) ≫ (constCone J X).π.app j = s.π.app j

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
m : s.pt ⟶ (constCone J X).pt
hm : ∀ (j : J), m ≫ (constCone J X).π.app j = s.π.app j
⊢ m = s.π.app (Classical.arbitrary J)

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
j x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ s.ι.app x✝¹ = s.ι.app x✝

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
j : J
⊢ s.ι.app (Classical.arbitrary J) = s.ι.app j

Tactic:
exact constant_of_preserves_morphisms _
      (fun _ _ f ↦ by simpa using (s.w f).symm) _ _

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
j : J
⊢ (constCocone J X).ι.app j ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
m : (constCocone J X).pt ⟶ s.pt
hm : ∀ (j : J), (constCocone J X).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app (Classical.arbitrary J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ ((𝟭 (C ⥤ D)).obj (incl ⋙ F)).map f ≫ F.map (starTerminal.from (of y)) =
    F.map (starTerminal.from (of x)) ≫ ((Functor.const C).obj (F.obj star)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c : Comma (𝟭 (C ⥤ D)) (Functor.const C)
x y : C
f : x ⟶ y
⊢ c.left.map f ≫ c.hom.app y = c.hom.app x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f✝ : x ⟶ y
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
⊢ ((ofCommaObject c).map f ≫
      match of a✝ with
      | of x => φ.left.app x
      | star => φ.right) =
    (match of a✝¹ with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map f

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
⊢ IsLimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
a : C
x✝ : of a ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.left.app x
      | star => φ.right) =
    (match of a with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map x✝

Tactic:
by

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ → G.map k₂ ≫ c.ι.app X₂ = G.map f ≫ c.ι.app Y → G.map k₁ ≫ c.ι.app X₁ = G.map f ≫ c.ι.app Y

Tactic:
intro _ _ _ _ _ h₁ h₂
    simp [← h₂, ← h₁, ← Functor.comp_map, c.ι.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
x✝ : star ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.left.app x
      | star => φ.right) =
    (match star with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map x✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ (extendCocone.obj c).ι.app X = G.map f ≫ c.ι.app Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ (incl ⋙ F).map f ≫ F.map (starTerminal.from (of y)) = F.map (starTerminal.from (of x))

Tactic:
simp only [Functor.comp_obj, Functor.comp_map]
          rw [← F.map_comp]
          congr 1

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ (incl ⋙ F).map f ≫ F.map (starTerminal.from (of y)) = F.map (starTerminal.from (of x))

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
hc : IsLimit c
this :
  limMap c.π =
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)).hom
⊢ IsIso (limMap c.π)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x : C
⊢ F.map (starTerminal.from (incl.obj x)) ≫ (Iso.refl (F.obj star)).hom =
    (Iso.refl (incl ⋙ F)).hom.app x ≫ F.map (starTerminal.from (of x))

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
hc : IsLimit c
⊢ IsIso (limMap c.π)

Tactic:
by

Goal state after: