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
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit G H
c : Cone (F ⋙ G)
hc : IsLimit (H.mapCone c)
hc' : IsLimit (extendCone.obj (H.mapCone c)) := (isLimitExtendConeEquiv F (H.mapCone c)).symm hc
⊢ ∀ (j : D),
    (extendCone.obj (H.mapCone c)).π.app j =
      (Iso.refl (extendCone.obj (H.mapCone c)).pt).hom ≫ (H.mapCone (extendCone.obj c)).π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.unop ⋯)
⊢ (pullbackIsoOpPushout f f).symm.hom ≫ pullback.snd f f =
    (pushout.inr f.unop f.unop).op ≫ (Iso.refl (Opposite.op (Opposite.unop X))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop X))).inv ≫ (ofπ f.unop.op ⋯).π ≫ (Iso.refl (ofπ f.unop.op ⋯).pt).hom =
    (ofπ f ⋯).π

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoUnopPullback f f).op.symm ≪≫ eqToIso ⋯).hom ≫ pullback.fst f.op f.op =
    (pushout.inl f f).op ≫ (Iso.refl (Opposite.op Y)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoUnopPullback f f).op.symm ≪≫ eqToIso ⋯).hom ≫ pullback.snd f.op f.op =
    (pushout.inr f f).op ≫ (Iso.refl (Opposite.op Y)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ (Iso.refl (Opposite.op Y)).inv ≫ (Cofork.ofπ f.op ⋯).π ≫ (Iso.refl (Cofork.ofπ f.op ⋯).pt).hom = (Cofork.ofπ f.op ⋯).π

Tactic:
by simp

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.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) := isLimitOfPreserves H ((isLimitWhiskerEquiv F c).symm hc)
⊢ ∀ (j : C),
    (H.mapCone (Cone.whisker F c)).π.app j =
      (Iso.refl (H.mapCone (Cone.whisker F c)).pt).hom ≫ (Cone.whisker F (H.mapCone c)).π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (ofι f.op.unop ⋯).pt).hom ≫ (ofι f ⋯).ι =
    (ofι f.op.unop ⋯).ι ≫ (Iso.refl (Opposite.unop (Opposite.op Y))).hom

Tactic:
by simp

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.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
hc' : IsLimit (Cone.whisker F (H.mapCone c)) := (isLimitWhiskerEquiv F (H.mapCone c)).symm hc
⊢ ∀ (j : C),
    (Cone.whisker F (H.mapCone c)).π.app j =
      (Iso.refl (Cone.whisker F (H.mapCone c)).pt).hom ≫ (H.mapCone (Cone.whisker F c)).π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯).hom ≫ pullback.fst f.unop f.unop =
    (pushout.inl f f).unop ≫ (Iso.refl (Opposite.unop Y)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯).hom ≫ pullback.snd f.unop f.unop =
    (pushout.inr f f).unop ≫ (Iso.refl (Opposite.unop Y)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ (Iso.refl (Opposite.unop Y)).inv ≫ (Cofork.ofπ f.unop ⋯).π ≫ (Iso.refl (Cofork.ofπ f.unop ⋯).pt).hom =
    (Cofork.ofπ f.unop ⋯).π

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (ofι f.unop.op ⋯).pt).hom ≫ (ofι f ⋯).ι =
    (ofι f.unop.op ⋯).ι ≫ (Iso.refl (Opposite.op (Opposite.unop Y))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ ∀ (s : Fork (𝟙 Y) (𝟙 Y)), (s.ι ≫ e.inv) ≫ (Fork.ofι e.hom ⋯).ι = s.ι

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y W : C
f : X ⟶ Y
inst✝ : IsRegularMono f
k : W ⟶ Y
h : k ≫ left f = k ≫ right f
m : W ⟶ X
hm : m ≫ f = k
⊢ lift f k h ≫ (Fork.ofι f ⋯).ι = k

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
⊢ ∀ (s : Fork g h), limit.lift (parallelPair g h) s ≫ (Fork.ofι (equalizer.ι g h) ⋯).ι = s.ι

Tactic:
by simp

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
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ (StructuredArrow.mk (f ≫ Final.homToLift F Y)).hom ≫ F.map (𝟙 (StructuredArrow.mk (f ≫ Final.homToLift F Y)).right) =
    f ≫ Final.homToLift F Y ≫ F.map (𝟙 (Final.lift F Y))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ ∀ (s : Cofork (𝟙 X) (𝟙 X)), (Cofork.ofπ e.hom ⋯).π ≫ e.inv ≫ s.π = s.π

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsRegularEpi f
k : X ⟶ Z
h : left f ≫ k = right f ≫ k
m : Y ⟶ Z
hm : f ≫ m = k
⊢ (Cofork.ofπ f ⋯).π ≫ desc f k h = k

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasColimit (parallelPair g h)
⊢ ∀ (s : Cofork g h), (Cofork.ofπ (coequalizer.π g h) ⋯).π ≫ colimit.desc (parallelPair g h) s = s.π

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasColimit (parallelPair g h)
s : Cofork g h
m : (Cofork.ofπ (coequalizer.π g h) ⋯).pt ⟶ s.pt
w : (Cofork.ofπ (coequalizer.π g h) ⋯).π ≫ m = s.π
⊢ m = colimit.desc (parallelPair g h) s

Tactic:
apply coequalizer.hom_ext
      simp [← w]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
S : C
k : IsKernelPair f a b
p q : S ⟶ X
w : p ≫ f = q ≫ f
⊢ k.lift p q w ≫ a = p ∧ k.lift p q w ≫ b = q

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)), small_k.lift s.fst s.snd ⋯ ≫ (PullbackCone.mk a b ⋯).fst = s.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)), small_k.lift s.fst s.snd ⋯ ≫ (PullbackCone.mk a b ⋯).snd = s.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ s.π.app WalkingCospan.left = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).fst

Tactic:
by simp

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((G ⋙ F).map (_root_.id (𝟙 bi))).toFunctor.obj
      (StructuredArrow.mk
            { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) }).right.fiber =
    (F.map gbi).toFunctor.obj f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ s.π.app WalkingCospan.right = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
by simp

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((G ⋙ F).map (_root_.id (𝟙 bj))).toFunctor.obj
      (StructuredArrow.mk
            { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).right.fiber =
    (F.map gbj).toFunctor.obj f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ diagonal f ≫ fst f f = diagonal f ≫ snd f f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ (p ≫ g) ≫ (Iso.refl X).hom = (Iso.refl A).hom ≫ p ≫ g

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ 𝟙 A ≫ (asIso p).hom = (Iso.refl A).hom ≫ p

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ 𝟙 X ≫ (asIso f).hom = (Iso.refl X).hom ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ (p ≫ g) ≫ (asIso f).hom = (asIso p).hom ≫ g ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst✝¹ : HasPullback v₂₂ f
H : P g
inst✝ : HasPullback (g ≫ v₂₂) f
⊢ pullback.fst (g ≫ v₂₂) f ≫ g =
    pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯ ≫ pullback.fst v₂₂ f

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := ⋯.equiv
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : R' ⊗[R] S
⊢ ↑R ↑e = f'.toLinearMap

Tactic:
exact ext' fun x y ↦ by simp [e, f', IsBaseChange.equiv_tmul, Algebra.smul_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
⊢ P f'

Tactic:
by
    have : HasPushout f g := sq.flip.hasPushout
    let e := sq.flip.isoPushout
    rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]
    exact hP₂ _ _ _ f g hf

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst✝¹ : HasPushout v₂₂ f
H : P g
inst✝ : HasPushout (v₂₂ ≫ g) f
⊢ pushout.inl v₂₂ f ≫ pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯ =
    g ≫ pushout.inl (v₂₂ ≫ g) f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g) ≫ 𝟙 Z = f ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)

Tactic:
change toMorphismProperty P _ ↔ toMorphismProperty P _

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) g
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.IsStableUnderLimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ ∀ (j : J), h₂.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f } ≫ c₂✝.π.app j = c₁✝.π.app j ≫ f.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ 𝟙 Y ≫ g ≫ f = g ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ (g ≫ f) ≫ 𝟙 S = g ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ f ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
⊢ f = 𝟙 X ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ (g ≫ f) ≫ 𝟙 S = g ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ f ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ (𝟙 X ≫ f) ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : Category.{t, w} J
X : C
P : ColimitPresentation J X
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
⊢ ∀ (j : J),
    (F.mapCocone { pt := X, ι := P.ι }).ι.app j ≫ (Iso.refl (F.mapCocone { pt := X, ι := P.ι }).pt).hom =
      { pt := F.obj X, ι := Functor.whiskerRight P.ι F ≫ (Functor.constComp J X F).hom }.ι.app j

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : Type w
inst✝³ : Category.{t, w} J✝
X✝ : C
J : Type w
inst✝² : Category.{t, w} J
X : C
P : LimitPresentation J X
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
⊢ ∀ (j : J),
    (F.mapCone { pt := X, π := P.π }).π.app j =
      (Iso.refl (F.mapCone { pt := X, π := P.π }).pt).hom ≫
        { pt := F.obj X, π := (Functor.constComp J X F).inv ≫ Functor.whiskerRight P.π F }.π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ diagonal f ≫ 𝟙 (diagonalObj f) = 𝟙 X ≫ diagonal f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝ : HasZeroObject C
⊢ ⊤ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
X Y : C
h : Retract Y X
hX : Q X
⊢ (h.r ≫ h.i) ≫ h.r ≫ h.i = h.r ≫ h.i

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
⊢ ∀ (j : J),
    (constCocone J (F.obj ⊥)).ι.app j ≫ c.ι.app ⊥ =
      { app := fun k ↦ F.map (homOfLE ⋯), naturality := ⋯ }.app j ≫ c.ι.app j

Tactic:
by simp

Goal state after: