mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ (s : Set (Subgroupoid C)), IsGLB s (sInf s)

Tactic:
by
      refine fun s => ⟨fun S Ss F => ?_, fun T Tl F fT => ?_⟩ <;> simp only [mem_sInf]
      exacts [fun hp => hp S Ss, fun S Ss => Tl Ss fT]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p = Groupoid.inv (Groupoid.inv p)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
Y : D
⊢ F.obj (F.objEquiv.symm Y) = Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ F.obj (F.objEquiv.symm X✝) = X✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ Y✝ = F.obj (F.objEquiv.symm Y✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
⊢ full ∅ = ⊥

Tactic:
by
  ext
  simp only [Bot.bot, mem_full_iff, mem_empty_iff_false, and_self_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J✝ : Type u_1
C✝ : Type u_2
inst✝⁵ : Category.{v_1, u_2} C✝
inst✝⁴ : Category.{v_2, u_1} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ C✝
inst✝³ : ChosenCoendsOfShape J✝ C✝
X✝ : C✝
f✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (G.obj (op j)).map φ
⊢ π F j' ≫ (F.map φ.op).app j' ≫ (f.app (op j)).app j' = π F j' ≫ (f.app (op j')).app j' ≫ (G.map φ.op).app j'

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
hx : (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ 0 = (ConcreteCategory.hom (colimit.ι F j)) 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
j' : J
i y : j ⟶ j'
g : (ConcreteCategory.hom (F.map i)) x = (ConcreteCategory.hom (F.map y)) 0
⊢ (ConcreteCategory.hom (F.map y)) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j ∈ {j, j', j''}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j' ∈ {j, j', j''}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j'' ∈ {j, j', j''}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ ⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩ ∈ {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
⊢ ∀ (j : Fin ((Opposite.unop Y✝).len + 1)),
    (U.cech.map f ≫ (U.cechIsoCechNerveApp hT Y✝).hom) ≫
        WidePullback.π (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom) j =
      ((U.cechIsoCechNerveApp hT X✝).hom ≫ (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.map f) ≫
        WidePullback.π (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom) j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ IsLimit (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone)

Tactic:
refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (BinaryBiproduct.isLimit (F.obj d) (G.obj d))
    · exact (pairComp F G ((evaluation D C).obj d)).symm
    · exact Cone.ext (Iso.refl _) <| by rintro (_ | _ | _) <;> cat_disch

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

Goal state before:
pp: case left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a✝ : C
⊢ F.map (𝟙 a✝) = 𝟙 (F.obj a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝² : Fan fun x ↦ U
x✝¹ : α
x✝ : x✝².pt.I
⊢ ({ f := fun i a ↦ (x✝².proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝².proj a).φ i } ≫ (U.powerFan α).proj x✝¹).f x✝ =
    (x✝².proj x✝¹).f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝¹ : Fan fun x ↦ U
x✝ : α
i✝ : x✝¹.pt.I
⊢ ({ f := fun i a ↦ (x✝¹.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝¹.proj a).φ i } ≫ (U.powerFan α).proj x✝).φ i✝ ≫
      eqToHom ⋯ =
    (x✝¹.proj x✝).φ i✝

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a✝ : D
⊢ G.map (𝟙 a✝) = 𝟙 (G.obj a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
x✝ : (monoFactorisation f).I.obj X
⊢ (ConcreteCategory.hom (H.m.app Y))
      ((ConcreteCategory.hom
            ((monoFactorisation f).I.map g ≫
              ↾fun x ↦
                match x with
                | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app Y)) (Exists.choose hx))).toFun
        x✝) =
    (ConcreteCategory.hom (H.m.app Y))
      ((ConcreteCategory.hom
            ((↾fun x ↦
                match x with
                | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx)) ≫
              H.I.map g)).toFun
        x✝)

Tactic:
simp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
x✝ : (monoFactorisation f).I.obj X
⊢ (ConcreteCategory.hom (f.app Y)) (Exists.choose ⋯) =
    (ConcreteCategory.hom (G.map g)) ((ConcreteCategory.hom (f.app X)) (Exists.choose ⋯))
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
x✝¹ : C
x✝ : (monoFactorisation f).I.obj x✝¹
⊢ (ConcreteCategory.hom
          (({
                  app := fun X ↦
                    ↾fun x ↦
                      match x with
                      | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx),
                  naturality := ⋯ } ≫
                H.m).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom ((monoFactorisation f).m.app x✝¹)).toFun x✝

Tactic:
simp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
x✝¹ : C
x✝ : (monoFactorisation f).I.obj x✝¹
⊢ (ConcreteCategory.hom (f.app x✝¹)) (Exists.choose ⋯) = ↑x✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
x✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).f x✝ = (U.powerπ (f a)).f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
i✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).φ i✝ ≫ eqToHom ⋯ = (U.powerπ (f a)).φ i✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
X✝ Y✝ Z✝ : FormalCoproduct C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
n✝ : SimplexCategoryᵒᵖ
⊢ { app := fun x ↦ powerMap (x✝¹ ≫ x✝) (ToType (Opposite.unop x)), naturality := ⋯ }.app n✝ =
    ({ app := fun x ↦ powerMap x✝¹ (ToType (Opposite.unop x)), naturality := ⋯ } ≫
          { app := fun x ↦ powerMap x✝ (ToType (Opposite.unop x)), naturality := ⋯ }).app
      n✝

Tactic:
simp

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

Goal state before:
pp: case h₁
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 F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclLeft C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclLeft C D).whiskerLeft α

Tactic:
simp

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

Goal state before:
pp: case h₂
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 F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclRight C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclRight C D).whiskerLeft α

Tactic:
simp

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

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ 𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫
      𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫
        𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫ 𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫ (mapPair Gₗ Gᵣ).map (𝟙 (left (Fₗ.obj c))) =
    𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
simp

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

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫
      𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫
        𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫ (mapPair Gₗ Gᵣ).map (𝟙 (right (Fᵣ.obj d))) =
    𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
simp

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

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mkNatTrans
          ((((whiskerRight (mapPairLeft Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fₗ.associator (inclLeft E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fₗ.whiskerLeft (mapPairLeft Gₗ Gᵣ).hom) ≫
              (Fₗ.associator Gₗ (inclLeft J K)).inv) ≫
            (mapPairLeft (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ((((whiskerRight (mapPairRight Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fᵣ.associator (inclRight E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fᵣ.whiskerLeft (mapPairRight Gₗ Gᵣ).hom) ≫
              (Fᵣ.associator Gᵣ (inclRight J K)).inv) ≫
            (mapPairRight (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ⋯).app
      (left c) =
    𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
simp

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

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mkNatTrans
          ((((whiskerRight (mapPairLeft Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fₗ.associator (inclLeft E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fₗ.whiskerLeft (mapPairLeft Gₗ Gᵣ).hom) ≫
              (Fₗ.associator Gₗ (inclLeft J K)).inv) ≫
            (mapPairLeft (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ((((whiskerRight (mapPairRight Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fᵣ.associator (inclRight E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fᵣ.whiskerLeft (mapPairRight Gₗ Gᵣ).hom) ≫
              (Fᵣ.associator Gᵣ (inclRight J K)).inv) ≫
            (mapPairRight (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ⋯).app
      (right d) =
    𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
simp

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

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
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
Fₗ Gₗ : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
αₗ : Fₗ ⟶ Gₗ
αᵣ : Fᵣ ⟶ Gᵣ
⊢ mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ = mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ

Tactic:
by
  ext
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i : Y.I
⊢ Y.obj i = Y.obj (e (e.symm i))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ factorThruImage (L.map f) ≫ (iso L f).hom = L.map (factorThruImage f)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝¹ : 𝒜
x✝ : (f x✝¹).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
          x✝¹).f
      x✝ =
    (p x✝¹).f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝ : 𝒜
i✝ : (f x✝).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
            x✝).φ
        i✝ ≫
      eqToHom ⋯ =
    (p x✝).φ i✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ (iso L f).inv ≫ image.ι (L.map f) = L.map (image.ι f)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i : X.I
⊢ X.objIsoOfEq ⋯ ≪≫ X.objIsoOfEq ⋯ = X.objIsoOfEq ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i : X.I
⊢ (X.objIsoOfEq ⋯).symm = X.objIsoOfEq ⋯

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
m : T ⟶ (pullbackCone f g pb).pt
⊢ (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd).1 ≫ f =
    (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd).2 ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case fst.h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
x✝ : T.I
⊢ (↑((fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩)
              ((fun s ↦
                  { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
                    φ := fun i ↦
                      (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
                s))).1.f
      x✝ =
    (↑s).1.f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
i✝ : T.I
⊢ (↑((fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩)
                ((fun s ↦
                    { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
                      φ := fun i ↦
                        (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
                  s))).1.φ
        i✝ ≫
      eqToHom ⋯ =
    (↑s).1.φ i✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case snd.h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
x✝ : T.I
⊢ (↑((fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩)
              ((fun s ↦
                  { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
                    φ := fun i ↦
                      (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
                s))).2.f
      x✝ =
    (↑s).2.f x✝

Tactic:
simp

Goal state after: