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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
      pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯ =
    𝟙 (pullback prod.snd f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ (pullbackProdSndIsoProd f Z).hom ≫ prod.fst = pullback.fst prod.snd f ≫ prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
g : StructuredArrow X (proj Y F)
⊢ X ⟶ (proj X (proj Y F) ⋙ proj Y F).obj g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ (pullbackProdSndIsoProd f Z).hom ≫ prod.snd = pullback.snd prod.snd f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ (pullbackProdSndIsoProd f Z).inv ≫ pullback.fst prod.snd f ≫ prod.fst = prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow X (proj Y F)
m : Y✝ ⟶ Z✝
⊢ Y✝.hom ≫ (proj X (proj Y F) ⋙ proj Y F).map m = Z✝.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ (pullbackProdSndIsoProd f Z).inv ≫ pullback.fst prod.snd f ≫ prod.snd = prod.snd ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ (pullbackProdSndIsoProd f Z).inv ≫ pullback.snd prod.snd f = prod.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow X (proj Y F)} (g : Y_1 ⟶ Z),
    Y_1.right.hom ≫ (Under.forget X ⋙ F).map (((proj X (proj Y F) ⋙ proj Y F).toUnder X (fun g ↦ g.hom) ⋯).map g) =
      Z.right.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
g : StructuredArrow Y (Under.forget X ⋙ F)
⊢ Y ⟶ F.obj ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).obj g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow Y (Under.forget X ⋙ F)
m : Y✝ ⟶ Z✝
⊢ Y✝.hom ≫ F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m) = Z✝.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
⊢ ∀ {Y_1 Z : StructuredArrow Y (Under.forget X ⋙ F)} (g : Y_1 ⟶ Z),
    Y_1.right.hom ≫
        (proj Y F).map
          (((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).toStructuredArrow Y F (fun g ↦ g.hom) ⋯).map g) =
      Z.right.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (g ≫ inv f) ≫ f = 𝟙 Y ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullbackConeOfLeftIso f g).π.app none = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
s : PullbackCone f g
⊢ s.snd ≫ (pullbackConeOfLeftIso f g).fst = s.fst ∧
    s.snd ≫ (pullbackConeOfLeftIso f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfLeftIso f g).pt},
        m ≫ (pullbackConeOfLeftIso f g).fst = s.fst → m ≫ (pullbackConeOfLeftIso f g).snd = s.snd → m = s.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ ≫ pullback.snd f g = 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
⊢ ∀ {X_1 Y_1 : StructuredArrow X (proj Y F)} (f : X_1 ⟶ Y_1),
    (𝟭 (StructuredArrow X (proj Y F))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow X (proj Y F))).obj Y_1)).hom =
      (Iso.refl ((𝟭 (StructuredArrow X (proj Y F))).obj X_1)).hom ≫
        (ofStructuredArrowProjEquivalence.functor F Y X ⋙ ofStructuredArrowProjEquivalence.inverse F Y X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsIso (pullback.snd f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
⊢ ∀ {X_1 Y_1 : StructuredArrow Y (Under.forget X ⋙ F)} (f : X_1 ⟶ Y_1),
    (ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).map f ≫
        (Iso.refl
            ((ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).obj
              Y_1)).hom =
      (Iso.refl
            ((ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).obj
              X_1)).hom ≫
        (𝟭 (StructuredArrow Y (Under.forget X ⋙ F))).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : StructuredArrow X (Functor.diag T)
g : Y✝ ⟶ Z✝
⊢ Y✝.hom.1 ≫ (proj X (Functor.diag T)).map g = Z✝.hom.1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ inv (pullback.snd f g) ≫ pullback.fst f g = g ≫ inv f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ 𝟙 X ≫ f = (f ≫ inv g) ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : StructuredArrow X (Functor.diag T)
g : Y✝ ⟶ Z✝
⊢ Y✝.hom.2 ≫ (Under.forget X.1).map (((proj X (Functor.diag T)).toUnder X.1 (fun f ↦ f.hom.1) ⋯).map g) = Z✝.hom.2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ (pullbackConeOfRightIso f g).π.app none = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
s : PullbackCone f g
⊢ s.fst ≫ (pullbackConeOfRightIso f g).fst = s.fst ∧
    s.fst ≫ (pullbackConeOfRightIso f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfRightIso f g).pt},
        m ≫ (pullbackConeOfRightIso f g).fst = s.fst → m ≫ (pullbackConeOfRightIso f g).snd = s.snd → m = s.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : StructuredArrow X.2 (Under.forget X.1)
m : Y✝ ⟶ Z✝
⊢ (Y✝.right.hom, Y✝.hom) ≫ (Functor.diag T).map ((proj X.2 (Under.forget X.1) ⋙ Under.forget X.1).map m) =
    (Z✝.right.hom, Z✝.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ pullback.lift (𝟙 X) (f ≫ inv g) ⋯ ≫ pullback.fst f g = 𝟙 X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
⊢ ∀ {X_1 Y : StructuredArrow X (Functor.diag T)} (f : X_1 ⟶ Y),
    (𝟭 (StructuredArrow X (Functor.diag T))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow X (Functor.diag T))).obj Y)).hom =
      (Iso.refl ((𝟭 (StructuredArrow X (Functor.diag T))).obj X_1)).hom ≫
        (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
⊢ ∀ {X_1 Y : StructuredArrow X.2 (Under.forget X.1)} (f : X_1 ⟶ Y),
    (ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).map f ≫
        (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj Y)).hom =
      (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj X_1)).hom ≫
        (𝟭 (StructuredArrow X.2 (Under.forget X.1))).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ IsIso (pullback.fst f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : StructuredArrow c (Comma.fst F G)
f : X✝ ⟶ Y✝
⊢ { left := Under.mk X✝.hom, right := X✝.right.right, hom := X✝.right.hom }.left.hom ≫ (Hom.right f).left =
    { left := Under.mk Y✝.hom, right := Y✝.right.right, hom := Y✝.right.hom }.left.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (pullback.fst f g) ≫ pullback.snd f g = f ≫ inv g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ f ≫ inv f ≫ g = g ≫ 𝟙 Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ (pushoutCoconeOfLeftIso f g).ι.app none = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
s : PushoutCocone f g
⊢ (pushoutCoconeOfLeftIso f g).inl ≫ s.inr = s.inl ∧
    (pushoutCoconeOfLeftIso f g).inr ≫ s.inr = s.inr ∧
      ∀ {m : (pushoutCoconeOfLeftIso f g).pt ⟶ s.pt},
        (pushoutCoconeOfLeftIso f g).inl ≫ m = s.inl → (pushoutCoconeOfLeftIso f g).inr ≫ m = s.inr → m = s.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : StructuredArrow c (Comma.fst F G)
f : X✝ ⟶ Y✝
⊢ (Under.forget c ⋙ F).map (Under.homMk (Hom.right f).left ⋯) ≫
      { left := Under.mk Y✝.hom, right := Y✝.right.right, hom := Y✝.right.hom }.hom =
    { left := Under.mk X✝.hom, right := X✝.right.right, hom := X✝.right.hom }.hom ≫ G.map (Hom.right f).right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inr f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ = 𝟙 Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
Y✝ Z✝ : Comma (Under.forget c ⋙ F) G
x✝ : Y✝ ⟶ Z✝
⊢ Y✝.left.hom ≫ (Comma.fst F G).map ((Comma.preLeft (Under.forget c) F G).map x✝) = Z✝.left.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
g : CostructuredArrow (proj F Y) X
⊢ (proj (proj F Y) X ⋙ proj F Y).obj g ⟶ X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (proj F Y) X
m : Y✝ ⟶ Z✝
⊢ (proj (proj F Y) X ⋙ proj F Y).map m ≫ Z✝.hom = Y✝.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (proj F Y) X} (g : Y_1 ⟶ Z),
    (Over.forget X ⋙ F).map (((proj (proj F Y) X ⋙ proj F Y).toOver X (fun g ↦ g.hom) ⋯).map g) ≫ Z.left.hom =
      Y_1.left.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
g : CostructuredArrow (Over.forget X ⋙ F) Y
⊢ F.obj ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).obj g) ⟶ Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ IsIso (pushout.inr f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y✝ ⟶ Z✝
⊢ F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫ Z✝.hom = Y✝.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inl f g ≫ inv (pushout.inr f g) = inv f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ f ≫ 𝟙 Y = g ≫ inv g ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ (pushoutCoconeOfRightIso f g).ι.app none = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
⊢ ∀ {Y_1 Z : CostructuredArrow (Over.forget X ⋙ F) Y} (g : Y_1 ⟶ Z),
    (proj F Y).map (((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).toCostructuredArrow F Y (fun g ↦ g.hom) ⋯).map g) ≫
        Z.left.hom =
      Y_1.left.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
⊢ ∀ {X_1 Y_1 : CostructuredArrow (proj F Y) X} (f : X_1 ⟶ Y_1),
    (𝟭 (CostructuredArrow (proj F Y) X)).map f ≫ (Iso.refl ((𝟭 (CostructuredArrow (proj F Y) X)).obj Y_1)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (proj F Y) X)).obj X_1)).hom ≫
        (ofCostructuredArrowProjEquivalence.functor F Y X ⋙ ofCostructuredArrowProjEquivalence.inverse F Y X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
s : PushoutCocone f g
⊢ (pushoutCoconeOfRightIso f g).inl ≫ s.inl = s.inl ∧
    (pushoutCoconeOfRightIso f g).inr ≫ s.inl = s.inr ∧
      ∀ {m : (pushoutCoconeOfRightIso f g).pt ⟶ s.pt},
        (pushoutCoconeOfRightIso f g).inl ≫ m = s.inl → (pushoutCoconeOfRightIso f g).inr ≫ m = s.inr → m = s.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
⊢ ∀ {X_1 Y_1 : CostructuredArrow (Over.forget X ⋙ F) Y} (f : X_1 ⟶ Y_1),
    (ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).map f ≫
        (Iso.refl
            ((ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).obj
              Y_1)).hom =
      (Iso.refl
            ((ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).obj
              X_1)).hom ≫
        (𝟭 (CostructuredArrow (Over.forget X ⋙ F) Y)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
g : CostructuredArrow (Functor.diag T) X
⊢ (proj (Functor.diag T) X).obj g ⟶ X.1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
⊢ (proj (Functor.diag T) X).map m ≫ Z✝.hom.1 = Y✝.hom.1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inl f g ≫ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ = 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
⊢ (Over.forget X.1).map (((proj (Functor.diag T) X).toOver X.1 (fun g ↦ g.hom.1) ⋯).map m) ≫ Z✝.hom.2 = Y✝.hom.2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Over.forget X.1) X.2
m : Y✝ ⟶ Z✝
⊢ (Functor.diag T).map ((proj (Over.forget X.1) X.2 ⋙ Over.forget X.1).map m) ≫ (Z✝.left.hom, Z✝.hom) =
    (Y✝.left.hom, Y✝.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
⊢ ∀ {X_1 Y : CostructuredArrow (Functor.diag T) X} (f : X_1 ⟶ Y),
    (𝟭 (CostructuredArrow (Functor.diag T) X)).map f ≫
        (Iso.refl ((𝟭 (CostructuredArrow (Functor.diag T) X)).obj Y)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (Functor.diag T) X)).obj X_1)).hom ≫
        (ofDiagEquivalence.functor X ⋙ ofDiagEquivalence.inverse X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
⊢ ∀ {X_1 Y : CostructuredArrow (Over.forget X.1) X.2} (f : X_1 ⟶ Y),
    (ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).map f ≫
        (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj Y)).hom =
      (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj X_1)).hom ≫
        (𝟭 (CostructuredArrow (Over.forget X.1) X.2)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : CostructuredArrow (Comma.fst F G) c
f : X✝ ⟶ Y✝
⊢ f.left.left ≫ { left := Over.mk Y✝.hom, right := Y✝.left.right, hom := Y✝.left.hom }.left.hom =
    { left := Over.mk X✝.hom, right := X✝.left.right, hom := X✝.left.hom }.left.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : CostructuredArrow (Comma.fst F G) c
f : X✝ ⟶ Y✝
⊢ (Over.forget c ⋙ F).map (Over.homMk f.left.left ⋯) ≫
      { left := Over.mk Y✝.hom, right := Y✝.left.right, hom := Y✝.left.hom }.hom =
    { left := Over.mk X✝.hom, right := X✝.left.right, hom := X✝.left.hom }.hom ≫ G.map f.left.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
Y✝ Z✝ : Comma (Over.forget c ⋙ F) G
x✝ : Y✝ ⟶ Z✝
⊢ (Comma.fst F G).map ((Comma.preLeft (Over.forget c) F G).map x✝) ≫ Z✝.left.hom = Y✝.left.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ IsIso (pushout.inl f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Over (op X)
f : Z ⟶ Y
⊢ (unop (op (Under.mk Y.hom.unop))).hom ≫ (Hom.left f).unop = (unop (op (Under.mk Z.hom.unop))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inr f g ≫ inv (pushout.inl f g) = inv g ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Under X)ᵒᵖ
f : Z ⟶ Y
⊢ (Under.Hom.right f.unop).op ≫ (mk (unop Y).hom.op).hom = (mk (unop Z).hom.op).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
⊢ Mono t.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
⊢ Mono t.fst

Tactic:
by

Goal state after: