mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).φ i✝ ≫ eqToHom ⋯ = (powerMap f α ≫ powerMap g α).φ i✝

Tactic:
dsimp

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
⊢ (Pi.map fun a ↦ f.φ (i✝ a) ≫ g.φ (f.f (i✝ a))) ≫ 𝟙 (∏ᶜ W.obj ∘ (f ≫ g).f ∘ i✝) =
    (Pi.map fun a ↦ f.φ (i✝ a)) ≫ Pi.map fun a ↦ g.φ (f.f (i✝ a))
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
b✝ : α
⊢ ((Pi.map fun a ↦ f.φ (i✝ a) ≫ g.φ (f.f (i✝ a))) ≫ 𝟙 (∏ᶜ W.obj ∘ (f ≫ g).f ∘ i✝)) ≫ Pi.π (W.obj ∘ g.f ∘ f.f ∘ i✝) b✝ =
    ((Pi.map fun a ↦ f.φ (i✝ a)) ≫ Pi.map fun a ↦ g.φ (f.f (i✝ a))) ≫ Pi.π (W.obj ∘ g.f ∘ f.f ∘ i✝) b✝

Tactic:
simp only [Category.comp_id, Category.assoc, Pi.map_π, Function.comp_apply,
      Pi.map_π_assoc]

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
b✝ : α
⊢ (Pi.map fun a ↦ f.φ (i✝ a) ≫ g.φ (f.f (i✝ a))) ≫ Pi.π (W.obj ∘ g.f ∘ f.f ∘ i✝) b✝ =
    Pi.π (U.obj ∘ i✝) b✝ ≫ f.φ (i✝ b✝) ≫ g.φ (f.f (i✝ b✝))
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

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

Tactic:
dsimp

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
i✝ : (U.power γ).I
⊢ (Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g (f x))) ≫ 𝟙 (∏ᶜ U.obj ∘ i✝ ∘ g ∘ f) =
    (Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g x)) ≫ Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝ ∘ g) (f x)
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

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

Tactic:
dsimp

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
i✝ : (U.power β).I
⊢ ((Pi.lift fun x ↦ Pi.π (U.obj ∘ i✝) (g x)) ≫ Pi.map fun a ↦ f.φ (i✝ (g a))) ≫ 𝟙 (∏ᶜ V.obj ∘ f.f ∘ i✝ ∘ g) =
    (Pi.map fun a ↦ f.φ (i✝ a)) ≫ Pi.lift fun x ↦ Pi.π (V.obj ∘ f.f ∘ i✝) (g x)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case refine_2
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
⊢ l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd

Tactic:
dsimp

Goal state after:
case refine_2
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
⊢ l ≫ G.hom.app i = s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case refine_3
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst
hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
k : J
⊢ (m ≫ ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }).π.app k) ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k).left.map f =
    { pt := s.1,
              π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }.π.app
        k ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k).left.map f

Tactic:
dsimp at *

Goal state after:
case refine_3
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ G.left.map f = s.fst
hm₂ : m ≫ G.hom.app i = s.snd
k : J
⊢ (m ≫ (Over.Hom.left (α.app k)).app i) ≫ (c.obj k).left.map f =
    ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯ ≫ (c.obj k).left.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
⊢ ((CatCommSq.iso F (ψ.comp φ).left (ψ.comp φ).base F'').hom ≫
          Functor.whiskerRight (Functor.whiskerRight α.left φ.left) F'').app
      x =
    (F.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫
          (CatCommSq.iso F (ψ'.comp φ).left (ψ'.comp φ).base F'').hom).app
      x

Tactic:
dsimp

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
⊢ (CatCommSq.iso F (ψ.left ⋙ φ.left) (ψ.base ⋙ φ.base) F'').hom.app x ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map (α.base.app (F.obj x)) ≫ (CatCommSq.iso F (ψ'.left ⋙ φ.left) (ψ'.base ⋙ φ.base) F'').hom.app x
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom ((F ⋙ P).map g)) ((fun j ↦ shrinkYonedaEquiv (c'.ι.app (op j) ≫ f)) X) =
    (fun j ↦ shrinkYonedaEquiv (c'.ι.app (op j) ≫ f)) X'

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    shrinkYonedaEquiv (c'.ι.app (op X') ≫ f)
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ (F.leftOp ⋙ shrinkYoneda.{w, v, u}).map f ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm ((ConcreteCategory.hom ((F ⋙ P).map f.unop)) (↑s (unop j₂))) ≫
      ((Functor.const Jᵒᵖ).obj P).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ shrinkYoneda.{w, v, u}.map (F.map f.unop).unop ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm ((ConcreteCategory.hom (P.map (F.map f.unop))) (↑s (unop j₂))) ≫ 𝟙 P
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
⊢ ((CatCommSq.iso G (ψ.comp φ).right (ψ.comp φ).base G'').hom ≫
          Functor.whiskerRight (Functor.whiskerRight α.right φ.right) G'').app
      x =
    (G.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫
          (CatCommSq.iso G (ψ'.comp φ).right (ψ'.comp φ).base G'').hom).app
      x

Tactic:
dsimp

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
⊢ (CatCommSq.iso G (ψ.right ⋙ φ.right) (ψ.base ⋙ φ.base) G'').hom.app x ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map (α.base.app (G.obj x)) ≫ (CatCommSq.iso G (ψ'.right ⋙ φ.right) (ψ'.base ⋙ φ.base) G'').hom.app x
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g✝ : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).sections
x✝¹ x✝ : ↑(Set.Iio j)
g : x✝¹ ⟶ x✝
⊢ (⋯.functor ⋙ hf.F).map g ≫ ↑s (op x✝) = ↑s (op x✝¹) ≫ ((Functor.const ↑(Set.Iio j)).obj Z).map g

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g✝ : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).sections
x✝¹ x✝ : ↑(Set.Iio j)
g : x✝¹ ⟶ x✝
⊢ hf.F.map (⋯.functor.map g) ≫ ↑s (op x✝) = ↑s (op x✝¹) ≫ 𝟙 Z
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f✝ : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f✝
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f✝
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ hf.F.map f ≫ ↑σ (op x✝) = ↑σ (op x✝¹) ≫ ((Functor.const J).obj Z).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f✝ : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f✝
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f✝
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ hf.F.map f ≫ ↑σ (op x✝) = ↑σ (op x✝¹) ≫ 𝟙 Z
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ { of := { of := T.η.app X.of }.of ≫ T.map f.of ≫ T.μ.app Y.of }.of = f.of

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ T.η.app X.of ≫ T.map f.of ≫ T.μ.app Y.of = f.of
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun x ↦ (ConcreteCategory.hom (f ≫ g).of) x) =
    (fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x

Tactic:
dsimp

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun x ↦ joinM (⇑(TypeCat.Hom.hom g.of) <$> (ConcreteCategory.hom f.of) x)) =
    (fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ Z
⊢ T.map (f ≫ g).of ≫ T.μ.app Z.of = (T.map f.of ≫ T.μ.app Y.of) ≫ T.map g.of ≫ T.μ.app Z.of

Tactic:
simp [← T.μ.naturality_assoc g.of, T.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj ((𝟭 C).obj A.A))

Tactic:
rw [← F.map_comp, ← F.map_id]
    exact congr_arg F.map A.unit

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))

Tactic:
dsimp

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj A.A)
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
dsimp

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (G.obj (F.obj A.A)) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)

Tactic:
dsimp

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit (parallelPair (G.map f) (G.map g)) (monadicLeftAdjoint G ⋙ G)
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit
    (parallelPair (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.left)
      (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)

Tactic:
dsimp

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit
    (parallelPair (G.map ((monadicLeftAdjoint G).map (G.map f))) (G.map ((monadicLeftAdjoint G).map (G.map g))))
    (monadicLeftAdjoint G ⋙ G)
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
c✝ c'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop c'✝ ⟶ unop c✝
g : unop d'✝ ⟶ unop d✝
⊢ (Quiver.Hom.unop (op f) ⊙ₗₘ Quiver.Hom.unop (op g)).op =
    (Quiver.Hom.unop (op f) ⊵ₗ unop d✝).op ≫ (unop c'✝ ⊴ₗ Quiver.Hom.unop (op g)).op

Tactic:
apply Quiver.Hom.unop_inj
        simpa [MonoidalLeftAction.action_exchange] using
          MonoidalLeftAction.actionHom_def f g

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Mon C
X : Cᵒᵖ
⊢ Small.{w, v} ↑((yonedaMon.obj M).obj X)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Mon C
X : Cᵒᵖ
⊢ Small.{w, v} (unop X ⟶ M.X)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Grp C
X : Cᵒᵖ
⊢ Small.{w, v} ↑((yonedaGrp.obj M).obj X)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Grp C
X : Cᵒᵖ
⊢ Small.{w, v} (unop X ⟶ M.X)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝³ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝² : C
x✝¹ : D
x✝ : Reflective R := { toFull := inst✝, toFaithful := inst✝¹, L := L, adj := adj }
this : IsIso adj.toMonad.μ
⊢ IsIso (adj.unit.app ((ihom x✝¹).obj (R.obj x✝²)))

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝³ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝² : C
x✝¹ : D
x✝ : Reflective R := { toFull := inst✝, toFaithful := inst✝¹, L := L, adj := adj }
this : IsIso adj.toMonad.μ
⊢ IsIso (adj.unit.app ((ihom x✝¹).obj (R.obj x✝²)))