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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
a : ι₂
⊢ c₂.inj a ≫ inj bc WalkingPair.right ≫ m =
    c₂.inj a ≫
      inj bc WalkingPair.right ≫
        IsColimit.desc h fun i ↦
          WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
            (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) (mkSelfProdFib F X) = t

Tactic:
rw [← piComparison_comp_π]
  simp [← PreservesProduct.iso_hom, mkSelfProdFib]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
let g : Aut (F.obj X) × F.obj X → F.obj X := fun ⟨σ, x⟩ ↦ σ.hom x
    let h (q : Aut F × F.obj X) : Aut (F.obj X) × F.obj X :=
      ⟨((fun p ↦ p X) ∘ autEmbedding F) q.1, q.2⟩
    change Continuous (g ∘ h)
    fun_prop

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ ↑((endEquivSectionsFibers F) f) A = (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
dsimp [endEquivSectionsFibers, Types.sectionsEquiv]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (↑((Types.limitEquivSections (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}))
            ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).toEquiv
              (((yoneda.obj (F ⋙ FintypeCat.incl)).mapIso
                    (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).op).toEquiv
                (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f))))
        A).down =
    (ConcreteCategory.hom (f.app A.obj)) A.pt
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
⊢ ∃ g, g • x = y

Tactic:
let F' : C ⥤ FintypeCat.{u₂} := F ⋙ FintypeCat.uSwitch.{w, u₂}
    let : FiberFunctor F' := FiberFunctor.comp_right _
    let e (Y : C) : F'.obj Y ≃ F.obj Y := (F.obj Y).uSwitchEquiv
    set x' : F'.obj X := (e X).symm x with hx'
    set y' : F'.obj X := (e X).symm y with hy'
    obtain ⟨g', (hg' : g'.hom.app X x' = y')⟩ := MulAction.exists_smul_eq (Aut F') x' y'
    let gapp (Y : C) : F.obj Y ≅ F.obj Y := FintypeCat.equivEquivIso <|
      (e Y).symm.trans <| (FintypeCat.equivEquivIso.symm (g'.app Y)).trans (e Y)
    let g : F ≅ F := NatIso.ofComponents gapp <| fun {X Y} f ↦ by
      ext x
      dsimp [gapp, e]
      erw [FintypeCat.uSwitchEquiv_naturality (F.map f)]
      rw [← Functor.comp_map]
      erw [← NatTrans.naturality_apply, FintypeCat.uSwitchEquiv_symm_naturality (F.map f)]
      rfl
    refine ⟨g, show (gapp X).hom x = y from ?_⟩
    simp [gapp, ← hx', hg', hy', Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
g σ : Aut F
⊢ (ConcreteCategory.hom
        ((coconeQuotientDiag h u hUinV).pt.ρ g ≫
          FintypeCat.homMk
            (Quotient.lift
              (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧)
              ⋯)))
      ⟦σ⟧ =
    (ConcreteCategory.hom
        (FintypeCat.homMk
            (Quotient.lift
              (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧)
              ⋯) ≫
          s.pt.ρ g))
      ⟦σ⟧

Tactic:
change (((Aut F ⧸ₐ U.toSubgroup).ρ g ≫ u.inv.hom) ≫ (s.ι.app (SingleObj.star _)).hom) ⟦σ⟧ =
      ((s.ι.app (SingleObj.star _)).hom ≫ s.pt.ρ g) (u.inv.hom ⟦σ⟧)

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
g σ : Aut F
⊢ (ConcreteCategory.hom
        (((ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))).ρ g ≫ u.inv.hom) ≫
          (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ⟦σ⟧ =
    (ConcreteCategory.hom ((s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom ≫ s.pt.ρ g))
      ((ConcreteCategory.hom u.inv.hom) ⟦σ⟧)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ d ∈ (im φ hφ).objs ↔ ∃ c, φ.obj c = d

Tactic:
by
  simp only [im, mem_map_objs_iff, mem_top_objs, true_and]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.whiskerLeft (X i₁) (β_ (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)).inv ≫
      MonoidalCategoryStruct.tensorHom (ιTensorObj X Z i₁ i₃ (i₁ + i₃) ⋯) (𝟙 (Y i₂)) ≫
        MonoidalCategoryStruct.tensorHom
            (tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i (i₁ + i₃) ⋯) (𝟙 (Y i₂)) ≫
          ιTensorObj (tensorObj Z X) Y (i₁ + i₃) i₂ k ⋯

Tactic:
← MonoidalCategory.comp_tensor_id_assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.whiskerLeft (X i₁) (β_ (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)).inv ≫
      MonoidalCategoryStruct.tensorHom
          (ιTensorObj X Z i₁ i₃ (i₁ + i₃) ⋯ ≫
            tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i (i₁ + i₃) ⋯)
          (𝟙 (Y i₂)) ≫
        ιTensorObj (tensorObj Z X) Y (i₁ + i₃) i₂ k ⋯
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (α_ f g h).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C (f ≫ g).toFunctor h.toFunctor)).hom ≫
        (Cat.Hom.isoMk (mapCompRight C f.toFunctor g.toFunctor)).hom ▷ (mapPair (𝟭 C) h.toFunctor).toCatHom ≫
          (α_ (mapPair (𝟭 C) f.toFunctor).toCatHom (mapPair (𝟭 C) g.toFunctor).toCatHom
                (mapPair (𝟭 C) h.toFunctor).toCatHom).hom ≫
            (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapCompRight C f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
by intros; exact congr($(mapWhiskerLeft_associator_hom C _ _ _).toCatHom₂)

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
n✝ : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject (FormalCoproduct C))).map (U.cechIsoCechNerve hT).hom ≫
          (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom).app
      n✝ =
    ((U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).hom ≫
          (SimplicialObject.const (FormalCoproduct C)).map
            (Iso.refl (U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).right).hom).app
      n✝

Tactic:
apply (isTerminalIncl _ hT).hom_ext

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 : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).f x✝ =
    (𝟙 X).f x✝

Tactic:
aesop

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 : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 X).φ i✝

Tactic:
aesop

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 : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).f x✝ =
    (𝟙 Y).f x✝

Tactic:
aesop

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 : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 Y).φ i✝

Tactic:
aesop

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 ⥤ α
⊢ Finset.univ.inf (K ⋙ (↑f).toFunctor).obj = f (finiteLimitCone K).cone.pt

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: case h₂
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
i✝ : ((incl C).obj X).I
⊢ (fromIncl (asSigma f).fst (asSigma f).snd).φ i✝ ≫ eqToHom ⋯ = f.φ i✝

Tactic:
aesop

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 subsingleton

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
⊢ image.lift { I := L.obj (image f), m := L.map (image.ι f), m_mono := ⋯, e := L.map (factorThruImage f), fac := ⋯ } ≫
      L.map (image.ι f) =
    image.ι (L.map f)

Tactic:
image.lift_fac

Goal state after:
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
⊢ image.ι (L.map f) = image.ι (L.map f)
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 ⥤ α
⊢ Finset.univ.sup (K ⋙ (↑f).toFunctor).obj = f (finiteColimitCocone K).cocone.pt

Tactic:
aesop

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

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:
cases a <;> simp

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:
cases a <;> simp

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:
cases a <;> simp

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 subsingleton

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

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 subsingleton

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

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 subsingleton

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

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

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (WithTerminal J) F
K✝ : J ⥤ Over X
coneK : Cone K✝
isLimitConeK : IsLimit coneK
isLimitConeD : IsLimit ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK)))
⊢ ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).π.app WithTerminal.star =
    (Iso.refl ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).pt).hom ≫
      (coneEquiv.functor.obj ((Over.post F).mapCone coneK)).π.app WithTerminal.star

Tactic:
aesop

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (WithTerminal J) F
K✝ : J ⥤ Over X
coneK : Cone K✝
isLimitConeK : IsLimit coneK
isLimitConeD : IsLimit ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK)))
a : J
⊢ ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).π.app (of a) =
    (Iso.refl ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).pt).hom ≫
      (coneEquiv.functor.obj ((Over.post F).mapCone coneK)).π.app (of a)

Tactic:
aesop

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (WithInitial J) F
K✝ : J ⥤ Under X
coconeK : Cocone K✝
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK)))
⊢ ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).ι.app
        WithInitial.star ≫
      (Iso.refl
          ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).pt).hom =
    (coconeEquiv.functor.obj ((Under.post F).mapCocone coconeK)).ι.app WithInitial.star

Tactic:
aesop

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
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : C ⥤ A
x : C
⊢ (Sigma.desc fun x_1 ↦ 𝟙 (F.obj (((incl C).obj x).obj x_1))) ≫ Sigma.ι (fun x_1 ↦ F.obj x) PUnit.unit =
    𝟙 (((eval C A ⋙ (whiskeringLeft C (FormalCoproduct C) A).obj (incl C)).obj F).obj x)

Tactic:
aesop

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (WithInitial J) F
K✝ : J ⥤ Under X
coconeK : Cocone K✝
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK)))
a : J
⊢ ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).ι.app (of a) ≫
      (Iso.refl
          ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).pt).hom =
    (coconeEquiv.functor.obj ((Under.post F).mapCocone coconeK)).ι.app (of a)

Tactic:
aesop

Goal state after: