mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ ∂R X Y Z = coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)

Tactic:
ext <;> simp [leftDistrib_hom, rightDistrib_hom]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (𝟙 (𝟙_ (Dial C)) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
by
  ext <;> simp; ext; simp; congr 1; ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (f ⊗ₘ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f

Tactic:
by
  ext <;> simp; ext; simp; congr 1; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F.toFunctor ≅ G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.hom.app a)
a : 𝒳.obj
this : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.inv.app a)

Tactic:
rw [← Iso.app_inv]

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F.toFunctor ≅ G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.hom.app a)
a : 𝒳.obj
this : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).inv
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip ⟶ R' ⋙ CostructuredArrow.grothendieckProj L ⋙ limit F

Tactic:
exact (limitCompWhiskeringLeftIsoCompLimit F (R' ⋙ CostructuredArrow.grothendieckProj L)).hom

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
| (F.map u ≫ F.map (coeqHom u v)).toFunctor.obj { base := c, fiber := f }.fiber

Tactic:
← F.map_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
| (F.map (u ≫ coeqHom u v)).toFunctor.obj { base := c, fiber := f }.fiber
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫
        enrichedComp V F₁ F₂ F₃ ≫
          precompEnrichedHom V F₁ F₃ (Under.forget j) ≫
            end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
          end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k

Tactic:
end_.lift_π,

Goal state after:
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫
        enrichedComp V F₁ F₂ F₃ ≫
          enrichedHomπ V F₁ F₃ ((Under.forget j).obj k) ≫
            eHomWhiskerRight V ((Iso.refl (Under.forget j ⋙ F₁)).inv.app k) (F₃.obj ((Under.forget j).obj k)) ≫
              eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj k) ((Iso.refl (Under.forget j ⋙ F₃)).hom.app k) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
          end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ (∀ (a : IsInitial X), False) ↔ Nonempty (F.obj X).obj

Tactic:
rw [← not_isEmpty_iff]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ (∀ (a : IsInitial X), False) ↔ ¬IsEmpty (F.obj X).obj
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ MonoCoprod C

Tactic:
exact MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono F

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this✝ : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this : IsIso (i ≫ (functorToAction F).map prod.fst)
⊢ IsIso (v.inv ≫ i ≫ (functorToAction F).map prod.fst)

Tactic:
apply IsIso.comp_isIso

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
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₂}

Goal state after:
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
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
⊢ ∃ g, g • x = y
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case htc
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (i : PointedGaloisObject F), IsClosed (cl i)

Tactic:
intro X
      apply IsClosed.leftCoset
      exact Subgroup.isClosed_of_isOpen _ (stabilizer_isOpen G X.pt)

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ (fun γ ↦ inv f ≫ γ ≫ f) ((fun δ ↦ f ≫ δ ≫ inv f) δ) = δ

Tactic:
by
    simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
      Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ StructuredArrow.hom Q ≫
      ((TwoSquare.overPost F X).costructuredArrowRightwards Z).map
        (CostructuredArrow.homMk
          (Over.homMk (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom) ⋯) ⋯) =
    StructuredArrow.hom P

Tactic:
by
        ext
        dsimp
        rw [← cancel_mono (prodComparison F X _)]
        ext
        · simpa [← Functor.map_comp, P] using Over.w Q.hom.left
        · simpa [← Functor.map_comp, P] using CostructuredArrow.w Q.hom

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
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ τ⁻¹ * σ⁻¹ * τ ∈ MulAction.stabilizer (Aut F) a

Tactic:
exact Subgroup.Normal.conj_mem hUnormal _ (Subgroup.inv_mem U.toSubgroup σinU) _

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Tactic:
· exact fun hf => S.mul hf hg

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
⊢ ∀ {c d e : C} {p : c ⟶ d},
    p ∈ {_f | c ∈ D ∧ d ∈ D} → ∀ {q : d ⟶ e}, q ∈ {_f | d ∈ D ∧ e ∈ D} → p ≫ q ∈ {_f | c ∈ D ∧ e ∈ D}

Tactic:
rintro _ _ _ _ ⟨⟩ _ ⟨⟩; constructor <;> assumption

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

Goal state before:
pp: case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ a✝ : C
g : (left a✝).Hom c
f : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c

Goal state after:
case left.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : C
f : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : C
f : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ : C
a✝ : D
g : (right a✝).Hom c
f : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c

Goal state after:
case left.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : C
a✝¹ : D
f : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : C
a✝¹ : D
f : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ : D
a✝ : C
g : (left a✝).Hom c
f : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c

Goal state after:
case right.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : D
a✝¹ : C
f : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : D
a✝¹ : C
f : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ a✝ : D
g : (right a✝).Hom c
f : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c

Goal state after:
case right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : D
f : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : D
f : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

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

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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ Nonempty h.Diagonal

Tactic:
apply LiftStruct.nonempty

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

case hf₁
C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ 𝟙 X ≫ f = f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: 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
k₁ k₂ : J
fk₁k₂ : k₁ ⟶ k₂
⊢ (((const J).obj s.1).map fk₁k₂ ≫ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k₂)).app j) s.snd ⋯) ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k₂).hom.app i =
    (⋯.lift (s.fst ≫ (Over.Hom.left (α.app k₁)).app j) s.snd ⋯ ≫
        (c ⋙ Over.forget F ⋙ (evaluation C D).obj i).map fk₁k₂) ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k₂).hom.app i

Tactic:
by simp [← NatTrans.comp_app]

Goal state after:
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''
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'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ ψ ◁ θ ≫ ψ ◁ inv θ = 𝟙 (ψ.comp φ)

Tactic:
simp [← whiskerLeft_comp]

Goal state after:
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''
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'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ ψ ◁ inv θ ≫ ψ ◁ θ = 𝟙 (ψ.comp φ')

Tactic:
simp [← whiskerLeft_comp]

Goal state after:
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''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ ψ ◁ θ ≫ ψ ◁ inv θ = 𝟙 (ψ.comp φ)

Tactic:
simp [← whiskerLeft_comp]

Goal state after:
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)
c : Cocone hf.F := { pt := Z, ι := { app := fun j ↦ ↑σ (op j), naturality := ⋯ } }
⊢ (fun g ↦ f ≫ g) (hf.isColimit.desc c) = g

Tactic:
by
        simp only [← hf.fac, Category.assoc, hf.isColimit.fac c ⊥, c, σ,
          d.sectionsMk_val_op_bot, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
⊢ L₂ ⋙ E'.inverse ≅ E.inverse ⋙ L₁

Tactic:
exact Iso.refl _

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 y : F ⊡ G
f : x ⟶ y
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst

Tactic:
by
  rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]

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

Goal state before:
pp: case mk
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : X ⟶ Y
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map (fun f ↦ Hom.whiskerLeft unit f) ⋯ (Quot.mk (⇑(X.setoidHom Y)) f) ≫
      { hom := ⟦Hom.l_hom Y⟧, inv := ⟦Hom.l_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    { hom := ⟦Hom.l_hom X⟧, inv := ⟦Hom.l_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ Quot.mk (⇑(X.setoidHom Y)) f

Tactic:
exact Quotient.sound (l_naturality _)

Goal state after: