mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : (c₁.map (F.flip.obj Y₂)).pt ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
l' : (c₂.map (F.obj c₁.pt)).pt ⟶ s.pt
hl' : Cofork.π (c₂.map (F.obj c₁.pt)) ≫ l' = l
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l' = Cofork.π s

Tactic:
by

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'
H : C ⥤ E
Fᵣ : D ⥤ E'
⊢ mapWhiskerLeft H (𝟙 Fᵣ) = 𝟙 (mapPair H Fᵣ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
⊢ ∃ l, (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = Cofork.π s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
⊢ Cofork.π (c₁.mapBifunctor c₂ F) ≫ ⋯.choose = s.π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
⊢ Cofork.π (c₁.mapBifunctor c₂ F) ≫ ⋯.choose = s.π

Tactic:
by simpa using (exists_desc hc₁ hc₂ F s).choose_spec

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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
m : (c₁.mapBifunctor c₂ F).pt ⟶ s.pt
hm : Cofork.π (c₁.mapBifunctor c₂ F) ≫ m = s.π
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ ⋯.choose

Tactic:
by

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
f g : X ⟶ Y
h₁ : f.f = g.f
i : X.I
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f : X.I → Y.I
F G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = { f := f, φ := G }.φ i
⊢ F = G

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f g : X ⟶ Y
h₁ : f.f = g.f
h₂ : ∀ (i : X.I), f.φ i ≫ eqToHom ⋯ = g.φ i
⊢ f = g

Tactic:
by

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ₗ
H : D ⥤ E'
⊢ (mapIsoWhiskerRight α H).inv = mapWhiskerRight α.inv H

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f g : X ⟶ Y
x✝ : f = g
⊢ ∃ (h₁ : f.f = f.f), ∀ (i : X.I), f.φ i ≫ eqToHom ⋯ = f.φ i

Tactic:
by

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
f g : X ⟶ Y
i : X.I
h₁ : f.f i = g.f i
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f g : X ⟶ Y
x✝ : f = g
⊢ ∀ (i : X.I), ∃ (h₁ : f.f i = f.f i), f.φ i ≫ eqToHom ⋯ = f.φ i

Tactic:
by

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:
by

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'
H : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
α : Fᵣ ≅ Gᵣ
⊢ (mapIsoWhiskerLeft H α).inv = mapWhiskerLeft H α.inv

Tactic:
by

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)
⊢ { f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } = 𝟙 X

Tactic:
by

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)
⊢ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom } = 𝟙 Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
⊢ fromIncl (asSigma f).fst (asSigma f).snd = f

Tactic:
by

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
⊢ L.map (factorThruImage f) ≫ L.map (image.ι f) = L.map f

Tactic:
by

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
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
m : (cofan 𝒜 f).pt ⟶ t
x✝ : (cofan 𝒜 f).pt.I
i : 𝒜
x : (f i).I
⊢ ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) m)).φ
        ⟨i, x⟩ ≫
      eqToHom ⋯ =
    m.φ ⟨i, x⟩

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁷ : FunLike F α β
f : F
inst✝⁶ : SemilatticeInf α
inst✝⁵ : OrderTop α
inst✝⁴ : SemilatticeInf β
inst✝³ : OrderTop β
inst✝² : InfTopHomClass F α β
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
K : J ⥤ α
⊢ ∀ (j : J),
    (finiteLimitCone (K ⋙ (↑f).toFunctor)).cone.π.app j =
      (eqToIso ⋯).hom ≫ ((↑f).toFunctor.mapCone (finiteLimitCone K).cone).π.app j

Tactic:
by

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).hom ≫ L.map (image.ι f) = image.ι (L.map f)

Tactic:
by

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
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
⊢ (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) = p

Tactic:
by

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
i : (X.toFun i✝).I
⊢ ((cofan X.I X.toFun).inj i✝ ≫ X.cofanPtIsoSelf.hom).φ i ≫ eqToHom ⋯ = (Hom.fromIncl i✝ (𝟙 (X.obj i✝))).φ i

Tactic:
by

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:
by

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
⊢ Sigma.ι X.toFun i ≫ X.coproductIsoSelf.hom = Hom.fromIncl i (𝟙 (X.obj i))

Tactic:
by

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
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X✝ X : FormalCoproduct C
i j : X.I
hij : i = j
⊢ X.obj i = X.obj j

Tactic:
by

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 j k : X.I
hij : i = j
hjk : j = k
⊢ X.objIsoOfEq hij ≪≫ X.objIsoOfEq hjk = X.objIsoOfEq ⋯

Tactic:
by

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 j : X.I
hij : i = j
⊢ (X.objIsoOfEq hij).symm = X.objIsoOfEq ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁷ : FunLike F α β
f : F
inst✝⁶ : SemilatticeSup α
inst✝⁵ : OrderBot α
inst✝⁴ : SemilatticeSup β
inst✝³ : OrderBot β
inst✝² : SupBotHomClass F α β
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
K : J ⥤ α
⊢ ∀ (j : J),
    (finiteColimitCocone (K ⋙ (↑f).toFunctor)).cocone.ι.app j ≫ (eqToIso ⋯).hom =
      ((↑f).toFunctor.mapCocone (finiteColimitCocone K).cocone).ι.app j

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
i : Function.Pullback f.f g.f
⊢ Z.obj (f.f (↑i).1) = Z.obj (g.f (↑i).2)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁴ : FunLike F α β
f : F
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : sInfHomClass F α β
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ α
⊢ (limitCone (K ⋙ (↑f).toFunctor)).cone.pt = ((↑f).toFunctor.mapCone (limitCone K).cone).pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁴ : FunLike F α β
f : F
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : sInfHomClass F α β
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ α
⊢ ∀ (j : J),
    (limitCone (K ⋙ (↑f).toFunctor)).cone.π.app j =
      (eqToIso ⋯).hom ≫ ((↑f).toFunctor.mapCone (limitCone K).cone).π.app j

Tactic:
by

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
i : { I := Function.Pullback f.f g.f, obj := fun i ↦ (pb i).pt }.I
⊢ ({ f := fun i ↦ (↑i).1, φ := fun i ↦ (pb i).fst } ≫ f).φ i ≫ eqToHom ⋯ =
    ({ f := fun i ↦ (↑i).2, φ := fun i ↦ (pb i).snd } ≫ g).φ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁴ : FunLike F α β
f : F
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : sSupHomClass F α β
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ α
⊢ (colimitCocone (K ⋙ (↑f).toFunctor)).cocone.pt = ((↑f).toFunctor.mapCocone (colimitCocone K).cocone).pt

Tactic:
by

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
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
e : C ≌ C'
e' : D ≌ D'
x : C ⋆ D
⊢ (mapPair e.functor e'.functor).map
        ((mapPairId.symm ≪≫
                mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                  mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                    mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
          x) ≫
      ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
              mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
        ((mapPair e.functor e'.functor).obj x) =
    𝟙 ((mapPair e.functor e'.functor).obj x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
inst✝⁴ : FunLike F α β
f : F
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : sSupHomClass F α β
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ α
⊢ ∀ (j : J),
    (colimitCocone (K ⋙ (↑f).toFunctor)).cocone.ι.app j ≫ (eqToIso ⋯).hom =
      ((↑f).toFunctor.mapCocone (colimitCocone K).cocone).ι.app j

Tactic:
by

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:
by

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
s : { p // p.1 ≫ f = p.2 ≫ g }
i : T.I
⊢ (↑s).1.φ i ≫
      f.φ (↑⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩) =
    (↑s).2.φ i ≫ g.φ (↑⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).2

Tactic:
by

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
i : T.I
⊢ (hpb ⟨((m ≫ (pullbackCone f g pb).fst).f i, (m ≫ (pullbackCone f g pb).snd).f i), ⋯⟩).lift
        (PullbackCone.mk ((m ≫ (pullbackCone f g pb).fst).φ i) ((m ≫ (pullbackCone f g pb).snd).φ i) ⋯) ≫
      (pb ⟨((m ≫ (pullbackCone f g pb).fst).f i, (m ≫ (pullbackCone f g pb).snd).f i), ⋯⟩).fst =
    m.φ i ≫ (pb ⟨((m ≫ (pullbackCone f g pb).fst).f i, (m ≫ (pullbackCone f g pb).snd).f i), ⋯⟩).fst

Tactic:
by

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
i : T.I
⊢ (hpb ⟨((m ≫ (pullbackCone f g pb).fst).f i, (m ≫ (pullbackCone f g pb).snd).f i), ⋯⟩).lift
        (PullbackCone.mk ((m ≫ (pullbackCone f g pb).fst).φ i) ((m ≫ (pullbackCone f g pb).snd).φ i) ⋯) ≫
      (pb ⟨((m ≫ (pullbackCone f g pb).fst).f i, (m ≫ (pullbackCone f g pb).snd).f i), ⋯⟩).snd =
    m.φ i ≫ (pb ⟨((m ≫ (pullbackCone f g pb).fst).f i, (m ≫ (pullbackCone f g pb).snd).f i), ⋯⟩).snd

Tactic:
by

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
i : T.I
⊢ ((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) ⋯) })
            ((fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩) m)).φ
        i ≫
      eqToHom ⋯ =
    m.φ i

Tactic:
by

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
s : { p // p.1 ≫ f = p.2 ≫ g }
⊢ (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) =
    s

Tactic:
by

Goal state after: