mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FinitePresentation

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

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasColimit F
c : Cocone F
inst✝ : IsIso (colimMap c.ι)
⊢ ∀ (j : J),
    (colimit.cocone F).ι.app j ≫
        (asIso (colimMap c.ι) ≪≫
            (colimit.isColimit ((Functor.const J).obj c.pt)).coconePointUniqueUpToIso
              (isColimitConstCocone J c.pt)).hom =
      c.ι.app j

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
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 (colimMap c.ι)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
⊢ (𝟭 (WithTerminal C ⥤ D)).map f ≫
      (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
          (Iso.refl (y.obj star)) ⋯).hom =
    (liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
          (Iso.refl (x.obj star)) ⋯).hom ≫
      ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
⊢ IsIso (colimMap c.ι)

Tactic:
by

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

Goal state before:
pp: J : Type v₁
⊢ IsConnected (WidePullbackShape J)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
⊢ { obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents
                (fun F ↦
                  liftUnique (incl ⋙ F) (fun x ↦ F.map (starTerminal.from (of x))) ⋯ F (Iso.refl (incl ⋙ F))
                    (Iso.refl (F.obj star)) ⋯)
                ⋯).hom.app
          x) ≫
      (NatIso.ofComponents
              (fun F ↦
                Iso.refl
                  (({ obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }).obj
                    F))
              ⋯).hom.app
        ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.obj x) =
    𝟙 ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.obj x)

Tactic:
by

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

Goal state before:
pp: J : Type v₁
⊢ IsConnected (WidePushoutShape J)

Tactic:
by

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

Goal state before:
pp: ⊢ IsConnected WalkingParallelPair

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : WithTerminal (Discrete J)
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x : WidePullbackShape J
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        x) =
    x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x : WithTerminal (Discrete J)
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        x) =
    x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
hc' : IsColimit (H.mapCocone (extendCocone.obj c)) := isColimitOfPreserves H ((isColimitExtendCoconeEquiv F c).symm hc)
⊢ ∀ (j : D),
    (H.mapCocone (extendCocone.obj c)).ι.app j ≫ (Iso.refl (H.mapCocone (extendCocone.obj c)).pt).hom =
      (extendCocone.obj (H.mapCocone c)).ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x y✝ : WidePullbackShape J
y : J
f : widePullbackShapeEquivObj none ⟶ widePullbackShapeEquivObj (some y)
⊢ none ⟶ some y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (extendCocone.obj (H.mapCocone c)) := (isColimitExtendCoconeEquiv F (H.mapCocone c)).symm hc
⊢ ∀ (j : D),
    (extendCocone.obj (H.mapCocone c)).ι.app j ≫ (Iso.refl (extendCocone.obj (H.mapCocone c)).pt).hom =
      (H.mapCocone (extendCocone.obj c)).ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
      ((prod.functor.obj X).mapCone c).π.app j =
    s.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x y : WidePullbackShape J
f : x ⟶ y
⊢ (fun f ↦
        match x, y, f with
        | some x, some y, f => cast ⋯ (Hom.id (some y))
        | none, some y, f => PEmpty.casesOn (fun t ↦ f = t → (none ⟶ some y)) f ⋯
        | some x, none, f => Hom.term x
        | none, none, f => Hom.id none)
      ((fun x_1 ↦
          match y, x, x_1 with
          | .(none), .(some j), Hom.term j => PUnit.unit
          | y, .(y), Hom.id .(y) => 𝟙 (widePullbackShapeEquivObj y))
        f) =
    f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x y✝ : WidePullbackShape J
y : J
f : widePullbackShapeEquivObj none ⟶ widePullbackShapeEquivObj (some y)
⊢ (fun x ↦
        match some y, none, x with
        | .(none), .(some j), Hom.term j => PUnit.unit
        | y, .(y), Hom.id .(y) => 𝟙 (widePullbackShapeEquivObj y))
      ((fun f ↦
          match none, some y, f with
          | some x, some y, f => cast ⋯ (Hom.id (some y))
          | none, some y, f => PEmpty.casesOn (fun t ↦ f = t → (none ⟶ some y)) f ⋯
          | some x, none, f => Hom.term x
          | none, none, f => Hom.id none)
        f) =
    f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
⊢ LiftableCocone (F ⋙ G) H c

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Final
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasColimit G
⊢ IsIso (colimit.pre G F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
X✝ Y✝ : WithTerminal (Discrete J)
f : X✝ ⟶ Y✝
⊢ widePullbackShapeEquivObj (widePullbackShapeEquivObj.symm X✝) = X✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Final
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasColimit G
X : C
⊢ colimit.ι (F ⋙ G) X ≫ (colimitIso F G).hom = colimit.ι G (F.obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
X✝ Y✝ : WithTerminal (Discrete J)
f : X✝ ⟶ Y✝
⊢ Y✝ = widePullbackShapeEquivObj (widePullbackShapeEquivObj.symm Y✝)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Final
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasColimit G
X : C
⊢ colimit.ι G (F.obj X) ≫ (colimitIso F G).inv = colimit.ι (F ⋙ G) X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x : WidePullbackShape J
⊢ (𝟭 (WidePullbackShape J)).obj x =
    ({ obj := ⇑widePullbackShapeEquivObj, map := fun {X Y} ↦ ⇑(widePullbackShapeEquivMap X Y), map_id := ⋯,
            map_comp := ⋯ } ⋙
          { obj := ⇑widePullbackShapeEquivObj.symm,
            map := fun {X Y} f ↦
              (widePullbackShapeEquivMap (widePullbackShapeEquivObj.symm X) (widePullbackShapeEquivObj.symm Y)).symm
                (eqToHom ⋯ ≫ f ≫ eqToHom ⋯),
            map_id := ⋯, map_comp := ⋯ }).obj
      x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : HasColimitsOfShape D E
inst✝ : HasColimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
⊢ ((whiskeringLeft C D E).obj F ⋙ colim).map f ≫ (colimitIso F Y✝).hom = (colimitIso F X✝).hom ≫ colim.map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x : WithTerminal (Discrete J)
⊢ ({ obj := ⇑widePullbackShapeEquivObj.symm,
            map := fun {X Y} f ↦
              (widePullbackShapeEquivMap (widePullbackShapeEquivObj.symm X) (widePullbackShapeEquivObj.symm Y)).symm
                (eqToHom ⋯ ≫ f ≫ eqToHom ⋯),
            map_id := ⋯, map_comp := ⋯ } ⋙
          { obj := ⇑widePullbackShapeEquivObj, map := fun {X Y} ↦ ⇑(widePullbackShapeEquivMap X Y), map_id := ⋯,
            map_comp := ⋯ }).obj
      x =
    (𝟭 (WithTerminal (Discrete J))).obj x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) := isColimitOfPreserves H ((isColimitWhiskerEquiv F c).symm hc)
⊢ ∀ (j : C),
    (H.mapCocone (Cocone.whisker F c)).ι.app j ≫ (Iso.refl (H.mapCocone (Cocone.whisker F c)).pt).hom =
      (Cocone.whisker F (H.mapCocone c)).ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
by

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

Goal state before:
pp: C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s))

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    (map (𝟭 C)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom ≫
        (𝟭 (WithInitial C)).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) := (isColimitWhiskerEquiv F (H.mapCocone c)).symm hc
⊢ ∀ (j : C),
    (Cocone.whisker F (H.mapCocone c)).ι.app j ≫ (Iso.refl (Cocone.whisker F (H.mapCocone c)).pt).hom =
      (H.mapCocone (Cocone.whisker F c)).ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : Y ⟶ X
inst✝ : EffectiveEpi f
Z✝¹ : C
m₁ m₂ : X ⟶ Z✝¹
h✝ : f ≫ m₁ = f ≫ m₂
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ Y
h : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ ≫ f ≫ m₂ = x✝ ≫ f ≫ m₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : Y ⟶ X
inst✝ : EffectiveEpi f
Z✝ : C
m₁ m₂ : X ⟶ Z✝
h : f ≫ m₁ = f ≫ m₂
⊢ m₁ = m₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : EffectiveEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
h : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ ≫ u = x✝ ≫ u

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : EffectiveEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
this : ∀ {Z : C} (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ u = g₂ ≫ u
⊢ f ≫ desc f u ⋯ ≫ z = f ≫ v

Tactic:
by

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₂
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ π a₁ ≫ m₂ = g₂ ≫ π a₂ ≫ m₂

Tactic:
by

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₂
⊢ m₂ = desc X π (fun a ↦ π a ≫ m₂) ⋯

Tactic:
by

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₂
⊢ m₁ = m₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
W✝ : C
e : Unit → (X ⟶ W✝)
h : ∀ {Z : C} (a₁ a₂ : Unit) (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W✝
hm : ∀ (a : Unit), f ≫ m = e a
⊢ m = desc f (e ()) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
E : Type u_2
inst✝¹ : Category.{v_1, u_1} D
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    (map (F ⋙ G)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom ≫
        (map F ⋙ map G).map f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit (F ⋙ G) H
c : Cocone (G ⋙ H)
hc : IsColimit c
⊢ LiftableCocone G H c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
⊢ FinitePresentation A B

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
⊢ ∀ ⦃X Y : WithInitial C⦄ (f : X ⟶ Y),
    ((map F).map f ≫
        match Y with
        | of x => η.app x
        | star => 𝟙 star) =
      (match X with
        | of x => η.app x
        | star => 𝟙 star) ≫
        (map G).map f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ ∀ (a : α), π a ≫ (asIso (Sigma.desc π)).inv ≫ Sigma.desc e = e a

Tactic:
by

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ : (X : C) × (d ⟶ F.obj X)
t : Relation.EqvGen (F ⋙ coyoneda.obj (op d)).ColimitTypeRel f₁ f₂
⊢ Zigzag (StructuredArrow.mk f₁.snd) (StructuredArrow.mk f₂.snd)

Tactic:
by

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
⊢ Nonempty (StructuredArrow d F)

Tactic:
by

Goal state after: