mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∀ (j : ↑(F.obj j✝)),
    colimit.ι (Grothendieck.ι F j✝ ⋙ X✝) j ≫
        colimit.ι ((fiberwiseColim F H).obj X✝) j✝ ≫
          (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
      colimit.ι (Grothendieck.ι F j✝ ⋙ X✝) j ≫
        colimit.ι ((fiberwiseColim F H).obj X✝) j✝ ≫ (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝

Tactic:
intro

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
j✝ : ↑(F.obj j✝¹)
⊢ colimit.ι (Grothendieck.ι F j✝¹ ⋙ X✝) j✝ ≫
      colimit.ι ((fiberwiseColim F H).obj X✝) j✝¹ ≫
        (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
    colimit.ι (Grothendieck.ι F j✝¹ ⋙ X✝) j✝ ≫
      colimit.ι ((fiberwiseColim F H).obj X✝) j✝¹ ≫ (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝
Module: Mathlib.CategoryTheory.Grothendieck

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

Tactic:
simp [down_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

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

Tactic:
simp [down_comp]

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 : D
⊢ ((𝟙 (G.functor ⋙ F)).app X).toFunctor =
    ((G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)).app X).toFunctor

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, Functor.id_obj,
      Functor.map_id, NatTrans.comp_app, NatTrans.id_app, whiskerLeft_app, whiskerRight_app,
      Equivalence.counitInv_functor_comp]

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
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)).hom

Tactic:
infer_instance

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✝ : HasColimit F
c : Cocone F
hc : IsColimit c
this :
  colimMap c.ι =
    ((colimit.isColimit F).coconePointUniqueUpToIso hc ≪≫
        (isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom
⊢ IsIso
    ((colimit.isColimit F).coconePointUniqueUpToIso hc ≪≫
        (isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom

Tactic:
infer_instance

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

Goal state before:
pp: case h.zero
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.zero ∈ p

Tactic:
t WalkingParallelPairHom.left

Goal state after:
case h.zero
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.one ∈ p
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
inst✝ : HasColimit G
⊢ IsIso
    ((colimit.isoColimitCocone (colimitCoconeComp F (getColimitCocone G))).hom ≫
      𝟙 (Cocone.whisker F (getColimitCocone G).cocone).pt ≫ (colimit.isoColimitCocone (getColimitCocone G)).inv)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ ∀ (a : α), π a ≫ m₂ = π a ≫ m₂

Tactic:
intro

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
a✝ : α
⊢ π a✝ ≫ m₂ = π a✝ ≫ m₂
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 G : C ⥤ D
η : F ⟶ G
X Y : WithInitial C
f✝ : X ⟶ Y
x y : C
f : of x ⟶ of y
⊢ ((map F).map f ≫
      match of y with
      | of x => η.app x
      | star => 𝟙 star) =
    (match of x with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map f

Tactic:
exact η.naturality f

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inr
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ x ∈ RingHom.ker f'.toRingHom

Tactic:
rw [← hs]

Goal state after:
case inr
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ x ∈ Ideal.span ↑s
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 : WithInitial C ⥤ D
x : C
⊢ (Iso.refl (F.obj star)).symm.hom ≫ F.map (starInitial.to (incl.obj x)) =
    F.map (starInitial.to (of x)) ≫ (Iso.refl (incl ⋙ F)).symm.hom.app x

Tactic:
simp only [Iso.refl_symm, Iso.refl_hom, Category.id_comp, Functor.comp_obj,
            NatTrans.id_app, Category.comp_id]; rfl

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
inst✝ : HasLimit G
⊢ IsIso (limit.isoLimitCone (limitConeComp F (getLimitCone G))).inv

Tactic:
infer_instance

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
hG :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
⊢ IsIso
    (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor) ≫
      colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsTerminal c
c' : C
this✝ : Inhabited (StructuredArrow c' (fromPUnit c)) := { default := StructuredArrow.mk (hc.from c') }
this : Subsingleton (StructuredArrow c' (fromPUnit c)) :=
  {
    allEq := fun i j ↦
      StructuredArrow.obj_ext i j (Subsingleton.elim i.right j.right)
        (IsTerminal.hom_ext hc (i.hom ≫ (fromPUnit c).map (eqToHom (Subsingleton.elim i.right j.right))) j.hom) }
⊢ IsConnected (StructuredArrow c' (fromPUnit c))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsInitial c
c' : C
this✝ : Inhabited (CostructuredArrow (fromPUnit c) c') := { default := CostructuredArrow.mk (hc.to c') }
this : Subsingleton (CostructuredArrow (fromPUnit c) c') :=
  {
    allEq := fun i j ↦
      CostructuredArrow.obj_ext i j (Subsingleton.elim i.left j.left)
        (IsInitial.hom_ext hc ((fromPUnit c).map (eqToHom (Subsingleton.elim i.left j.left)) ≫ j.hom) i.hom) }
⊢ IsConnected (CostructuredArrow (fromPUnit c) c')

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
⊢ (ker f).FG

Tactic:
have : ker f = ⊥ := by rw [← RingHom.injective_iff_ker_eq_bot]; exact hf.1

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
this : ker f = ⊥
⊢ (ker f).FG
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
⊢ m = p

Tactic:
have z := w.trans hp₁.symm

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
⊢ m = p
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : SplitEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
this : IsSplitEpi f
⊢ IsRegularEpi f

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : IsRegularEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
this : IsRegularEpi f
⊢ StrongEpi f

Tactic:
infer_instance

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
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (inv (fst f f))

Tactic:
infer_instance

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

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C
F : C₀ ⥤ C
X : C
inst✝ : F.Initial
Y : Over X
⊢ IsConnected (CostructuredArrow F Y.left)

Tactic:
infer_instance

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✝ : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv

Tactic:
infer_instance

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

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ fst f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst f f

pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ snd f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd f f

Tactic:
· simp only [Category.assoc, diagonal_fst, Category.comp_id, limit.lift_π,
          PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_left]

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ snd f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd f f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_5
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) ⋯ ⋯)
⊢ IsIso
    (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
      (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
      (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ⋯)

Tactic:
infer_instance

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderCobaseChange → P.pushouts ≤ P

Tactic:
intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩
    exact of_isPushout h₂ h₁

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))
⊢ IsStableUnderBaseChange P

Tactic:
by
  introv R h H
  let e := h.symm.1.equiv
  let f' := Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S')
    (IsScalarTower.toAlgHom R S S')
  have hef (x : _) : e x = f' x := by
    suffices e.toLinearMap.restrictScalars R = f'.toLinearMap from congr($this x)
    exact ext' fun x y ↦ by simp [e, f', IsBaseChange.equiv_tmul, Algebra.smul_def]
  have hemul (x y : _) : e (x * y) = e x * e y := by simp_rw [hef, map_mul]
  convert! h₁.1 _ { e with map_mul' := hemul } (h₂ H)
  ext x
  simp [e, h.symm.1.equiv_tmul, Algebra.smul_def]

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

Goal state before:
pp: case refine_2.refine_3
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) ⋯ ⋯)
⊢ IsIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)

Tactic:
infer_instance

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_1
inst✝ : Category.{v_1, u_1} J
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
hφ : ∀ (j : J), h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ W.limitsOfShape J (h₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
exact ⟨_, _, _, _, h₁, _, _, hf⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
f : Fin 0 → C
this : PreservesLimitsOfShape (Discrete (Fin 0)) F :=
  preservesLimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv'.symm) F
⊢ PreservesLimit (Discrete.functor f) F

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝⁵ : Category.{v', u'} J
J' : Type u''
inst✝⁴ : Category.{v'', u''} J'
inst✝³ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝² : LocallySmall.{w, v_1, u_1} C
inst✝¹ : Small.{w, u'} J
inst✝ : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (P.strictLimitsOfShape J).isoClosure

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
⊢ ∀ (j : Discrete (Fin (n + 1))),
    (extendCofan c₁ c₂).ι.app j ≫
        ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
            (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
      s.ι.app j

Tactic:
by
    rintro ⟨j⟩
    refine Fin.inductionOn j ?_ ?_
    · apply (BinaryCofan.IsColimit.desc' t₂ _ _).2.1
    · rintro i -
      dsimp only [extendCofan_ι_app]
      rw [Fin.cases_succ, assoc, (BinaryCofan.IsColimit.desc' t₂ _ _).2.2, t₁.fac]
      rfl

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 }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
choose X Y h hX using fun (a : Subtype R) ↦ a.2

Goal state after:
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 }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
f : Fin 0 → C
this : PreservesColimitsOfShape (Discrete (Fin 0)) F :=
  preservesColimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv'.symm) F
⊢ PreservesColimit (Discrete.functor f) F

Tactic:
infer_instance

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_1
inst✝ : Category.{v_1, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ MorphismProperty.isomorphisms C φ

Tactic:
have := NatIso.isIso_of_isIso_app f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : IsIso f
⊢ MorphismProperty.isomorphisms C φ
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z X Y : C
f : X ⟶ Y
inst✝¹ : HasPushout f f
inst✝ : Epi f
⊢ IsIso (inv (inl f f))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
⊢ P X

Tactic:
by
    let c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r (by simp)
    have hc : IsColimit c :=
      Cofork.IsColimit.mk _ (fun s ↦ h.i ≫ s.π)
        (fun s ↦ by simpa using! s.condition)
        (fun s m hm ↦ by dsimp [c] at hm; simp [← hm])
    exact P.prop_of_isColimit hc (by rintro (_ | _) <;> exact hY)

Goal state after: