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

Goal state before:
pp: case e_a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } =
    ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
        { base := g,
          fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
      { base := eqToHom ⋯, fiber := eqToHom ⋯ }

Tactic:
fapply Grothendieck.ext

Goal state after:
case e_a.w_base
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }.base =
    (({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
        { base := eqToHom ⋯, fiber := eqToHom ⋯ }).base

case w_fiber
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ eqToHom ⋯ ≫ { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }.fiber =
    (({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
        { base := eqToHom ⋯, fiber := eqToHom ⋯ }).fiber
Module: Mathlib.RingTheory.FinitePresentation

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

Tactic:
intro _ _ _ _ h₁ h₂
        exact add_mem h₁ h₂

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 G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ (map (whiskerRight α Cat.asSmallFunctor)).map f ≫ (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom =
    (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f

Tactic:
fapply Grothendieck.ext

Goal state after:
case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
        (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom).base =
    ((Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f).base

case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫
      ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
          (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom).fiber =
    ((Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f).fiber
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:
fapply Grothendieck.ext

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

case w_fiber
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✝
⊢ eqToHom ⋯ ≫
      ((pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom).fiber =
    (({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f).fiber
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
        (eqToHom ⋯ ≫
          ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                  (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
              X ≫
            (𝟙
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                    pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
              X) ≫
      (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
    𝟙 ((pre F G.functor).obj X)

Tactic:
fapply Grothendieck.ext

Goal state after:
case w_base
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
          (eqToHom ⋯ ≫
            ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                    (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                X ≫
              (𝟙
                    (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                      pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).base =
    (𝟙 ((pre F G.functor).obj X)).base

case w_fiber
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)
⊢ eqToHom ⋯ ≫
      ((pre F G.functor).map
            (eqToHom ⋯ ≫
              ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                      (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                  X ≫
                (𝟙
                      (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                        pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                  X) ≫
          (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).fiber =
    (𝟙 ((pre F G.functor).obj X)).fiber
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star.of.unit
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) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ G.map PUnit.unit ≫
      (match of Y with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map PUnit.unit

Tactic:
change G.map _ ≫ h.hom.app _ = hG.hom ≫ _

Goal state after:
case star.of.unit
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) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ G.map PUnit.unit ≫ h.hom.app Y = hG.hom ≫ (lift F M hM).map PUnit.unit
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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j : C
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₂ ≫ G.map k₂ = s.π.app j → s.π.app X₁ ≫ G.map k₁ = s.π.app j

Tactic:
intro j₁ j₂ k₁ k₂ f w h
    rw [← s.w f] at h
    rw [← w]
    simpa using h

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_3
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
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ adjoin R (Set.range MvPolynomial.X) →
      y ∈ adjoin R (Set.range MvPolynomial.X) →
        x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
          y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
            x + y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
intro _ _ _ _ h₁ h₂
        exact add_mem h₁ h₂

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)
m : s.pt ⟶ (Fork.ofι e.hom ⋯).pt
w : m ≫ (Fork.ofι e.hom ⋯).ι = s.ι
⊢ m = s.ι ≫ e.inv

Tactic:
by simp [← w]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case zero
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ (ker (g'.comp MvPolynomial.C)).FG

Tactic:
← comap_ker

Goal state after:
case zero
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ (Ideal.comap MvPolynomial.C (ker g')).FG
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ IsColimit
    (PushoutCocone.mk (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)
      ⋯)

Tactic:
apply botSquareIsPushout _ rfl (pushoutIsPushout _ g₄)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ IsColimit
    ((PushoutCocone.mk (pushout.inl g₃ g₄) (pushout.inr g₃ g₄) ⋯).pasteVert
      (PushoutCocone.mk (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
          (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)
        ⋯)
      ⋯)
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case refine_1
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cocone D
hc : IsColimit c
j : J
inst✝ : (Under.forget j).Final
this : Nonempty (Under j)
c'' : Cocone
  (Under.lift (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)) :=
  Under.liftCocone (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
hc'' : IsColimit c'' :=
  Under.isColimitLiftCocone (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯ ((Functor.Final.isColimitWhiskerEquiv (Under.forget j) c).symm hc)
⊢ Under.lift (Under.forget j ⋙ D)
      ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D) ≅
    Under.post D

Tactic:
exact NatIso.ofComponents (fun k ↦ CategoryTheory.Under.isoMk (Iso.refl _))

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
⊢ ∀ (f g : Arrow C) (x : f ≅ g), P f.hom → P g.hom

Tactic:
intro f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
f : Arrow C
⊢ ∀ (g : Arrow C) (x : f ≅ g), P f.hom → P g.hom
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ EssentiallySmall.{u, v, max (v + 1) u} (FGAlgCat R)

Tactic:
suffices h : EssentiallySmall.{u} (FGAlgCat.{max u v} R) by
    exact essentiallySmall_of_fully_faithful (FGAlgCat.uliftFunctor R)
  rw [essentiallySmall_iff]
  refine ⟨?_, ?_⟩
  · let f := toSkeleton ∘ (FGAlgCat.uliftFunctor R).obj ∘ FGAlgCatSkeleton.eval R
    refine small_of_surjective (f := f) fun A ↦ ?_
    simp only [Function.comp_apply, f, toSkeleton_eq_iff]
    obtain ⟨P, ⟨e⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R
      ((fromSkeleton (FGAlgCat R)).obj A).obj
    exact ⟨P, ⟨ObjectProperty.isoMk _ (CommAlgCat.isoMk <| ULift.algEquiv.trans e.symm)⟩⟩
  · refine ⟨fun A B ↦ ?_⟩
    obtain ⟨PA, ⟨eA⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R A.obj
    obtain ⟨PB, ⟨eB⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R B.obj
    let f (g : A ⟶ B) (x : PA.eval.obj) : PB.eval.obj := eB (g.hom (eA.symm x))
    refine small_of_injective (f := f) fun u v h ↦ ?_
    ext a
    obtain ⟨a, rfl⟩ := eA.symm.surjective a
    exact eB.injective (congr_fun h a)

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
n : ℕ
this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
⊢ ∀ (f : Fin (n + 1) → C), PreservesLimit (Discrete.functor f) F

Tactic:
intro f

Goal state after:
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
n : ℕ
this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ PreservesLimit (Discrete.functor f) F
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)
⊢ (extendCofan c₁ c₂).pt ⟶ s.pt

Tactic:
apply (BinaryCofan.IsColimit.desc' t₂ (s.ι.app ⟨0⟩) _).1
    apply t₁.desc ⟨_, Discrete.natTrans fun i => s.ι.app ⟨i.as.succ⟩⟩

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✝ : P.ContainsZero
⊢ ∃ X, IsZero X

Tactic:
obtain ⟨X, h₁, h₂⟩ := P.exists_prop_of_containsZero

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝ : P.ContainsZero
X : C
h₁ : IsZero X
h₂ : P X
⊢ ∃ X, IsZero X
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
n : ℕ
this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
⊢ ∀ (f : Fin (n + 1) → C), PreservesColimit (Discrete.functor f) F

Tactic:
intro f

Goal state after:
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
n : ℕ
this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ PreservesColimit (Discrete.functor f) F
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
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯ ≫
        lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
          (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯) ≫
      snd f g =
    𝟙 (pullback f g) ≫ snd f g

Tactic:
· simp only [Category.assoc, lift_snd, lift_snd_assoc, Category.id_comp]

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✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
⊢ W α

Tactic:
by
    let φ := fun j => f.app (Discrete.mk j)
    have : HasColimit X₁ := ⟨c₁, hc₁⟩
    have : HasColimit X₂ := ⟨c₂, hc₂⟩
    have : HasCoproduct fun j ↦ X₁.obj (Discrete.mk j) :=
      hasColimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₁.obj j)))
    have : HasCoproduct fun j ↦ X₂.obj (Discrete.mk j) :=
      hasColimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₂.obj j)))
    have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))
    refine (W.arrow_mk_iso_iff ?_).1 hf'
    refine Arrow.isoMk
      ((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₁) hc₁)
      ((Sigma.isoColimit _) ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit X₂) hc₂) ?_
    apply colimit.hom_ext
    rintro ⟨j⟩
    simp [φ, hα]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
G X : C
inst✝ : GrpObj G
A B : C
e : G ≅ X
⊢ lift (e.inv ≫ ι ≫ e.hom) (𝟙 X) ≫ μ = toUnit X ≫ η

Tactic:
by simp +instances [MonObj.ofIso]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
G X : C
inst✝ : GrpObj G
A B : C
e : G ≅ X
⊢ lift (𝟙 X) (e.inv ≫ ι ≫ e.hom) ≫ μ = toUnit X ≫ η

Tactic:
by simp +instances [MonObj.ofIso]

Goal state after: