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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.op ⋙ coyoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((colimitHomIsoLimitYoneda' (D.op ⋙ coyoneda) F).hom ≫
          limit.π ((D.op ⋙ coyoneda).rightOp ⋙ yoneda.obj F) i ≫
            ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i))) (𝟙 (D.obj i))) }

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.op ⋙ coyoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((yoneda.obj F).map (colimit.ι (D.op ⋙ coyoneda) (op i)).op ≫
          ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i))) (𝟙 (D.obj i))) }
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F).hom ≫
          limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ yoneda.obj F) i ≫
            ((D ⋙ Prod.sectL Cᵒᵖ F).isoWhiskerLeft (yonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((yoneda.obj F).map (colimit.ι (D.leftOp ⋙ yoneda) (op i)).op ≫
          ((D ⋙ Prod.sectL Cᵒᵖ F).isoWhiskerLeft (yonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ ExactAt I.cocomplex (n + 1)

Tactic:
← quasiIsoAt_iff_exactAt I.ι (n + 1) (exactAt_succ_single_obj _ _)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt I.ι (n + 1)
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0

Tactic:
w,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ (I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom) ((ConcreteCategory.hom q) a'') = a

Tactic:
dsimp at ha' ⊢

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom) ((ConcreteCategory.hom q) a'') = a
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom x.hom) ((ConcreteCategory.hom p) a'') = a

Tactic:
dsimp at ha' ⊢

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom x.hom) ((ConcreteCategory.hom p) a'') = a
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (P.ι ≫ g).f 0 = f ≫ Q.ι.f 0

Tactic:
w,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ ((CochainComplex.single₀ C).map f ≫ Q.ι).f 0 = f ≫ Q.ι.f 0
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ r • F.map f✝ ≫ α.app Y✝ = r • α.app X✝ ≫ G.map f✝

Tactic:
α.naturality

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ r • α.app X✝ ≫ G.map f✝ = r • α.app X✝ ≫ G.map f✝
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h) =
    StructuredArrow.hom (t.whisker h)

Tactic:
rw [← cancel_mono (α_ _ _ _).inv]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = (f.core s ∪ f.Domᶜ) ∩ (f.Domᶜ ∪ f.Dom)

Tactic:
Set.compl_union_self,

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = (f.core s ∪ f.Domᶜ) ∩ Set.univ
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      none =
    ↑(ConcreteCategory.hom f.hom) none

pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
· exact f.hom.map_snd.symm

Goal state after:
case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
⊢ (hom
        ((homDiagram
              ((hom
                  (limit.lift (F ⋙ objects)
                    { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                X✝)
              ((hom
                  (limit.lift (F ⋙ objects)
                    { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                Y✝)).map
          h))
      (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
dsimp [Functor.comp_obj, homDiagram_obj]

Goal state after:
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
⊢ eqToHom ⋯ ≫ (F.map h).toFunctor.map (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ ≫ ψ = τ
⊢ (π' ≫ φ) ≫ ψ = τ

Tactic:
simp only [assoc, hπ'₂]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst✝ : p.IsCocartesian f φ'
⊢ IsCocartesian.map p f φ' φ ≫ IsCocartesian.map p f φ φ' = 𝟙 b'

Tactic:
subst_hom_lift p f φ'
    apply IsCocartesian.ext p (p.map φ') φ'
    simp only [fac_assoc, fac, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FintypeCat

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (∏ᶜ X).obj
i : ι
⊢ (productEquiv X) x i = (ConcreteCategory.hom (Pi.π X i)) x

Tactic:
by
  simpa [productEquiv, equivEquivIso, equivIsoIso, Iso.toEquiv] using!
    piComparison_comp_π_apply FintypeCat.incl X i x

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsGalois A
a b : (F.obj A).obj
⊢ (ConcreteCategory.hom (F.map ((evaluationEquivOfIsGalois F A a).symm b).hom)) a = b

Tactic:
change (evaluationEquivOfIsGalois F A a) _ = _
  simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha✝ : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
this : Fintype (fι ⟨X, XinI⟩)
x : (F.obj X).obj
j : fι ⟨X, XinI⟩
a : ((Discrete.functor (ff ⟨X, XinI⟩) ⋙ F).obj { as := j }).obj
ha : (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a = x
⊢ (ConcreteCategory.hom (σ.hom.app X))
      ((ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a) =
    (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a

Tactic:
NatTrans.naturality_apply

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha✝ : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
this : Fintype (fι ⟨X, XinI⟩)
x : (F.obj X).obj
j : fι ⟨X, XinI⟩
a : ((Discrete.functor (ff ⟨X, XinI⟩) ⋙ F).obj { as := j }).obj
ha : (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a = x
⊢ (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j })))
      ((ConcreteCategory.hom (σ.hom.app ((Discrete.functor (ff ⟨X, XinI⟩)).obj { as := j }))) a) =
    (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: 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
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x

Tactic:
let P : C := ∏ᶜ X

Goal state after:
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
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J✝ : Type u_1
C✝ : Type u_2
inst✝⁵ : Category.{v_1, u_2} C✝
inst✝⁴ : Category.{v_2, u_1} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ C✝
inst✝³ : ChosenCoendsOfShape J✝ C✝
X✝ : C✝
f✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (G.obj (op j)).map φ
⊢ π F j ≫ (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = π F j' ≫ (f.app (op j')).app j' ≫ (G.map φ.op).app j'

Tactic:
reassoc_of% chosenEnd.condition F φ

Goal state after:
J✝ : Type u_1
C✝ : Type u_2
inst✝⁵ : Category.{v_1, u_2} C✝
inst✝⁴ : Category.{v_2, u_1} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ C✝
inst✝³ : ChosenCoendsOfShape J✝ C✝
X✝ : C✝
f✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (G.obj (op j)).map φ
⊢ π F j' ≫ (F.map φ.op).app j' ≫ (f.app (op j)).app j' = π F j' ≫ (f.app (op j')).app j' ≫ (G.map φ.op).app j'
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 (Hom.left u ≫ X.hom) = toUnit A ≫ curryRightUnitorHom I

Tactic:
w,

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 ≫ (ihom I).map ((toOver I).obj A).hom = toUnit A ≫ curryRightUnitorHom I
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ { toFun := fun f ↦ f.of, invFun := fun f ↦ { of := f }, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
    (toKleisli T).map f ≫ { toFun := fun f ↦ f.of, invFun := fun f ↦ { of := f }, left_inv := ⋯, right_inv := ⋯ }.symm g

Tactic:
ext
        simp [← T.η.naturality_assoc g]

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ (tensorRight Y.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) =
    (tensorRight Y.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((ρ_ X).hom ▷ Y)

Tactic:
apply (initialIsInitial.ofIso ((initialIsoIsInitial ?_) ≪≫ (mulZero ?_).symm)).hom_ext <;>
    exact initialIsInitial.ofIso (zeroMul initialIsInitial).symm

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      η ▷ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
    𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom

Tactic:
slice_lhs 1 2 => rw [whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (η ▷ (P.X ⊗ Q.X) ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ actLeft P Q =
    𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (α_ (𝟙_ C) P.X Q.X).inv ≫
      (λ_ P.X).hom ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (λ_ (P.X ⊗ Q.X)).hom ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      μ ▷ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
    (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫
        R.X ◁ actLeft P Q ≫ actLeft P Q

Tactic:
slice_lhs 1 2 => rw [whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (μ ▷ (P.X ⊗ Q.X) ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ actLeft P Q =
    (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫
        R.X ◁ actLeft P Q ≫ actLeft P Q