mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
⊢ t ∈ ↑(MulAction.stabilizer (Aut F) { obj := A, pt := a, isGalois := hgal }.pt) → t ∈ S

Tactic:
(ht : t.hom.app A a = a)

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
⊢ t ∈ S
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p q : X ⟶ Y
⊢ HomRel.CompClosure redStep p q → HomRel.CompClosure redStep (Path.reverse p) (Path.reverse q)

Tactic:
by
  rintro ⟨_, _, XW, _, _, WY, _, _, f⟩
  have : HomRel.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
      (WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) := by
    constructor
    constructor
  simpa only [CategoryStruct.comp, CategoryStruct.id, Quiver.Path.reverse, Quiver.Path.nil_comp,
    Quiver.Path.reverse_comp, Quiver.reverse_reverse, Quiver.Path.reverse_toPath,
    Quiver.Path.comp_assoc] using this

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S✝ x✝¹ x✝ : Subgroupoid C
S : (c d : C) → Set (c ⟶ d)
inv✝¹ : ∀ {c d : C} {p : c ⟶ d}, p ∈ S c d → Groupoid.inv p ∈ S d c
mul✝¹ : ∀ {c d e : C} {p : c ⟶ d}, p ∈ S c d → ∀ {q : d ⟶ e}, q ∈ S d e → p ≫ q ∈ S c e
T : (c d : C) → Set (c ⟶ d)
inv✝ : ∀ {c d : C} {p : c ⟶ d}, p ∈ T c d → Groupoid.inv p ∈ T d c
mul✝ : ∀ {c d e : C} {p : c ⟶ d}, p ∈ T c d → ∀ {q : d ⟶ e}, q ∈ T d e → p ≫ q ∈ T c e
h : ↑{ arrows := S, inv := inv✝¹, mul := mul✝¹ } = ↑{ arrows := T, inv := inv✝, mul := mul✝ }
c d : C
f : c ⟶ d
⊢ f ∈ { arrows := S, inv := inv✝¹, mul := mul✝¹ }.arrows c d ↔ f ∈ { arrows := T, inv := inv✝, mul := mul✝ }.arrows c d

Tactic:
apply Set.ext_iff.1 h ⟨c, d, f⟩

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
rw [SetLike.le_def, Sigma.forall]; exact forall_congr' fun c => Sigma.forall

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ {p | Discrete.Arrows c d p} → Groupoid.inv p ∈ {p | Discrete.Arrows d c p}

Tactic:
rintro _ _ _ ⟨⟩; simp only [inv_eq_inv, IsIso.inv_id]; constructor

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.disconnect.IsTotallyDisconnected

Tactic:
rw [isTotallyDisconnected_iff]; exact fun c d ⟨_, h, _⟩ => h

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

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

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x✝ : (F ⨿ G).obj a
⊢ (fun z ↦ (hom ((binaryCoproductIso F G).inv.app a)) z) ((fun z ↦ (hom ((binaryCoproductIso F G).hom.app a)) z) x✝) =
    x✝

Tactic:
by simp [-coprod_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x✝ : F.obj a ⊕ G.obj a
⊢ (fun z ↦ (hom ((binaryCoproductIso F G).hom.app a)) z) ((fun z ↦ (hom ((binaryCoproductIso F G).inv.app a)) z) x✝) =
    x✝

Tactic:
by simp [-coprod_obj]

Goal state after:
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' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
x : P.obj c.pt
x✝ : Jᵒᵖ
⊢ c'.ι.app x✝ ≫ coconePtToShrinkYoneda c hc' ≫ shrinkYonedaEquiv.symm x =
    c'.ι.app x✝ ≫ (coconeCompShrinkYonedaHomEquiv hc').symm (Types.sectionOfCone (P.mapCone c) x)

Tactic:
dsimp [coconePtToShrinkYoneda, coconeCompShrinkYonedaHomEquiv_symm_apply]

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' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
x : P.obj c.pt
x✝ : Jᵒᵖ
⊢ c'.ι.app x✝ ≫ hc'.desc (shrinkYoneda.{w, v, u}.mapCocone (coconeLeftOpOfCone c)) ≫ shrinkYonedaEquiv.symm x =
    c'.ι.app x✝ ≫
      hc'.desc
        { pt := P,
          ι :=
            { app := fun j ↦ shrinkYonedaEquiv.symm (↑(Types.sectionOfCone (P.mapCone c) x) (unop j)),
              naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hᵣ
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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).snd = (β.app x).snd

Tactic:
exact congrArg (fun t ↦ t.app x) e₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
⊢ (toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh) = CatCommSqOver.mkIso e₁ e₂ ⋯

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case id_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ ((Hom.id X✝).comp f✝) = projectMapAux f✝¹ f✝

Tactic:
dsimp only [projectMapAux]; rw [Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
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₂
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
φ φ' : CatCospanTransform F₁ G₁ F₂ G₂
α : φ ⟶ φ'
⊢ (transform X).map (ψ ◁ α) =
    (transformObjComp X ψ φ).hom ≫
      ((transform X).obj ψ).whiskerLeft ((transform X).map α) ≫ (transformObjComp X ψ φ').inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
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₂
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
α : ψ ⟶ ψ'
φ : CatCospanTransform F₁ G₁ F₂ G₂
⊢ (transform X).map (α ▷ φ) =
    (transformObjComp X ψ φ).hom ≫
      whiskerRight ((transform X).map α) ((transform X).obj φ) ≫ (transformObjComp X ψ' φ).inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
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₂
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₃
X : Type u₁₃
inst✝ : Category.{v₁₃, u₁₃} X
ψ : CatCospanTransform F G F₁ G₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
⊢ (transform X).map (α_ ψ φ τ).hom =
    (transformObjComp X (ψ.comp φ) τ).hom ≫
      whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ) ≫
        (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom ≫
          ((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv ≫ (transformObjComp X ψ (φ.comp τ)).inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
⊢ (transform X).map (λ_ ψ).hom =
    (transformObjComp X (CatCospanTransform.id F G) ψ).hom ≫
      whiskerRight (transformObjId X F G).hom ((transform X).obj ψ) ≫ ((transform X).obj ψ).leftUnitor.hom

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
⊢ (transform X).map (ρ_ ψ).hom =
    (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)).hom ≫
      ((transform X).obj ψ).whiskerLeft (transformObjId X F₁ G₁).hom ≫ ((transform X).obj ψ).rightUnitor.hom

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
V W : Y ⥤ Z
α : V ⟶ W
⊢ (precompose F G).map (U.whiskerLeft α) =
    (precomposeObjComp F G U V).hom ≫
      whiskerRight ((precompose F G).map α) ((precompose F G).obj U) ≫ (precomposeObjComp F G U W).inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
⊢ (precompose F G).map (whiskerRight α W) =
    (precomposeObjComp F G U W).hom ≫
      ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
⊢ (precompose F G).map (U.associator V W).hom =
    (precomposeObjComp F G (U ⋙ V) W).hom ≫
      ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
        (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
          whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫ (precomposeObjComp F G U (V ⋙ W)).inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
⊢ (precompose F G).map U.leftUnitor.hom =
    (precomposeObjComp F G (𝟭 X) U).hom ≫
      ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫ ((precompose F G).obj U).rightUnitor.hom

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
⊢ (precompose F G).map U.rightUnitor.hom =
    (precomposeObjComp F G U (𝟭 Y)).hom ≫
      whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫ ((precompose F G).obj U).leftUnitor.hom

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U V : X ⥤ Y
α : U ⟶ V
⊢ whiskerRight ((precompose F G).map α) ((transform X).obj ψ) ≫
      (CatCommSq.iso ((precompose F G).obj V) ((transform Y).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj V)).hom =
    (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj U)).hom ≫
      ((transform Y).obj ψ).whiskerLeft ((precompose F₁ G₁).map α)

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
ψ : CatCospanTransform F G F₁ G₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
⊢ (CatCommSq.iso ((precompose F G).obj (𝟭 X)) ((transform X).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj (𝟭 X))).hom ≫
      ((transform X).obj ψ).whiskerLeft (precomposeObjId F₁ G₁ X).hom =
    whiskerRight (precomposeObjId F G X).hom ((transform X).obj ψ) ≫
      ((transform X).obj ψ).leftUnitor.hom ≫ ((transform X).obj ψ).rightUnitor.inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
X : Type u₇
Y : Type u₈
Z : Type u₉
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
V : Y ⥤ Z
⊢ (CatCommSq.iso ((precompose F G).obj (U ⋙ V)) ((transform Z).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj (U ⋙ V))).hom ≫
      ((transform Z).obj ψ).whiskerLeft (precomposeObjComp F₁ G₁ U V).hom =
    whiskerRight (precomposeObjComp F G U V).hom ((transform X).obj ψ) ≫
      (((precompose F G).obj V).associator ((precompose F G).obj U) ((transform X).obj ψ)).hom ≫
        ((precompose F G).obj V).whiskerLeft
            (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
                ((precompose F₁ G₁).obj U)).hom ≫
          (((precompose F G).obj V).associator ((transform Y).obj ψ) ((precompose F₁ G₁).obj U)).inv ≫
            whiskerRight
                (CatCommSq.iso ((precompose F G).obj V) ((transform Z).obj ψ) ((transform Y).obj ψ)
                    ((precompose F₁ G₁).obj V)).hom
                ((precompose F₁ G₁).obj U) ≫
              (((transform Z).obj ψ).associator ((precompose F₁ G₁).obj V) ((precompose F₁ G₁).obj U)).hom

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry (β_ I A).hom ≫ (ihom I).map ((toOver I).obj A).hom = toUnit A ≫ curryRightUnitorHom I

Tactic:
← curry_natural_right,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry ((β_ I A).hom ≫ ((toOver I).obj A).hom) = toUnit A ≫ curryRightUnitorHom I
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
⊢ whiskerRight ((transform Y).map η) ((precompose F₁ G₁).obj U) ≫
      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
          ((transform X).obj ψ')).hom =
    (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
          ((transform X).obj ψ)).hom ≫
      ((precompose F G).obj U).whiskerLeft ((transform X).map η)

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
⊢ (CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
          ((transform X).obj (CatCospanTransform.id F G))).hom ≫
      ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom =
    whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
      ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.inv

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
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₂
X : Type u₁₀
Y : Type u₁₁
inst✝¹ : Category.{v₁₀, u₁₀} X
inst✝ : Category.{v₁₁, u₁₁} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
⊢ (CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
          ((transform X).obj (ψ.comp ψ'))).hom ≫
      ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom =
    whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
      (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
        ((transform Y).obj ψ).whiskerLeft
            (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                ((transform X).obj ψ')).hom ≫
          (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
            whiskerRight
                (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                    ((transform X).obj ψ)).hom
                ((transform X).obj ψ') ≫
              (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom

Tactic:
by
  ext <;> simp

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
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
B : D
⊢ (comparisonAdjunction adj).counit.app B =
    colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
      (counitCofork adj B)

Tactic:
apply coequalizer.hom_ext
  change
    coequalizer.π _ _ ≫ coequalizer.desc ((adj.homEquiv _ B).symm (𝟙 _)) _ =
      coequalizer.π _ _ ≫ coequalizer.desc _ _
  simp [Adjunction.homEquiv_counit]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : BimonObj M
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ M M (M ⊗ M)).hom ≫
        M ◁ (α_ M M M).inv ≫ M ◁ (β_ M M).hom ▷ M ≫ M ◁ (α_ M M M).hom ≫ (α_ M M (M ⊗ M)).inv ≫ (μ ⊗ₘ μ) =
    μ ≫ Δ

Tactic:
simp only [BimonObj.mul_comul, tensorμ, Category.assoc]

Goal state after: