mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) 0

Tactic:
rw [CochainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros]

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
              ((CochainComplex.single₀ C).obj Z)).X₂,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
        X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
        f :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
              (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
        g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
        zero := ⋯ }.Exact ∧
    Mono
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
          (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂

case zero.hf₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).f = 0

case zero.hg₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).g = 0

case zero.hf₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).f = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
⊢ P (Abelian.image f)

Tactic:
rw [← exists_comp_monoModSerre_eq_zero_iff P]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h : ∀ (j : Discrete ι), f ≫ { hom := ↾fun x ↦ x j.as, comm := ⋯ } = s.π.app j
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom f.hom) x j = (ConcreteCategory.hom (s.π.app { as := j }).hom) x

Tactic:
← h ⟨j⟩

Goal state after:
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h : ∀ (j : Discrete ι), f ≫ { hom := ↾fun x ↦ x j.as, comm := ⋯ } = s.π.app j
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom f.hom) x j = (ConcreteCategory.hom (f ≫ { hom := ↾fun x ↦ x { as := j }.as, comm := ⋯ }).hom) x
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ { V := F.obj X✝.V, ρ := { toFun := fun g ↦ F.map (X✝.ρ g), map_one' := ⋯, map_mul' := ⋯ } }.ρ g ≫ F.map f.hom =
    F.map f.hom ≫ { V := F.obj Y✝.V, ρ := { toFun := fun g ↦ F.map (Y✝.ρ g), map_one' := ⋯, map_mul' := ⋯ } }.ρ g

Tactic:
dsimp; rw [← F.map_comp, f.comm, F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj Y) (F.obj Y)ᘁ ≫ (inv (F.map f) ≫ F.map f) ▷ (F.obj Y)ᘁ

Tactic:
IsIso.inv_hom_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj Y) (F.obj Y)ᘁ ≫ 𝟙 (F.obj Y) ▷ (F.obj Y)ᘁ
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this✝ : Continuous v
u : H × ↑((forget₂ (ContAction V H) TopCat).obj X) → ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.obj.ρ p.1))) p.2
this : Continuous u
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
change Continuous (u ∘ v)

Goal state after:
V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this✝ : Continuous v
u : H × ↑((forget₂ (ContAction V H) TopCat).obj X) → ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.obj.ρ p.1))) p.2
this : Continuous u
⊢ Continuous (u ∘ v)
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)

Tactic:
· ext
    dsimp
    rw [← Functor.map_comp, X.unit, Functor.map_id]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ({ obj := fun t ↦ ∐ fun x ↦ x✝, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ x✝) (g ≫ f), map_id := ⋯,
              map_comp := ⋯ }.map
          f_1 ≫
        Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) =
      (Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) ≫
        { obj := fun t ↦ ∐ fun x ↦ d₂, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ d₂) (g ≫ f),
              map_id := ⋯, map_comp := ⋯ }.map
          f_1

Tactic:
intros
        dsimp
        ext
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (adj₂.homEquiv X (F.obj Y'))
      (F.map (L.map g ≫ ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h)) ≫ adj₁.counit.app (F.obj Y')) =
    g ≫
      ↑((Fork.IsLimit.homIso
            (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y)
          ((Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
            ⟨(adj₂.homEquiv Y (F.obj Y'))
                (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')),
              ⋯⟩))

Tactic:
simp only [Fork.ofι_pt, Functor.map_comp, assoc, limit.cone_x]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (adj₂.homEquiv X (F.obj Y'))
      (F.map (L.map g) ≫
        F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')) =
    g ≫
      ↑((Fork.IsLimit.homIso
            (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y)
          ((Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
            ⟨(adj₂.homEquiv Y (F.obj Y'))
                (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')),
              ⋯⟩))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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 : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
⊢ (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint

Tactic:
by
    refine ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft ?_).isLeftAdjoint
    exact Functor.isoWhiskerLeft L (Comonad.comparisonForget (comonadicAdjunction F)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (g.comp g✝)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g✝))

Tactic:
ihg (f.comp g),

Goal state after:
case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ (normalizeAux nil (f.comp g)).comp (normalizeAux nil g✝) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g✝))
Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f g : F X ⟶ F Y
h : f = g
⊢ mkHom₂ (eqToHom h) = eqToHom ⋯

Tactic:
by
  ext; subst h; simp only [eqToHom_refl, Hom.category_id_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.map (𝟙 { as := { as := () } }) ◁ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
          F.map (𝟙 { as := { as := () } }) ◁ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) =
    F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ▷ F.map (𝟙 { as := { as := () } }) ≫
          F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ▷ F.map (𝟙 { as := { as := () } }) ≫
            (α_ (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
                (F.map (𝟙 { as := { as := () } }))).hom

Tactic:
rw [← F.mapComp_naturality_left_assoc, ← F.mapComp_naturality_right_assoc]

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.map₂ (𝟙 { as := { as := () } } ◁ (ρ_ (𝟙 { as := { as := () } })).inv) ≫
        F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } } ≫ 𝟙 { as := { as := () } }) ≫
          F.map (𝟙 { as := { as := () } }) ◁ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) =
    F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.map₂ ((ρ_ (𝟙 { as := { as := () } })).inv ▷ 𝟙 { as := { as := () } }) ≫
        F.mapComp (𝟙 { as := { as := () } } ≫ 𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
          F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ▷ F.map (𝟙 { as := { as := () } }) ≫
            (α_ (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
                (F.map (𝟙 { as := { as := () } }))).hom
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ ((LeftLift.mk f adj.unit).whisker h).unit ≫ (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ▷ u =
    𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
dsimp only [whisker_lift, StructuredArrow.mk_right, whisker_unit,
          StructuredArrow.mk_hom_eq_self]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ (h ◁ adj.unit ≫ (α_ h f u).inv) ≫ (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ▷ u =
    𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u)
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
    (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
rw [F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).hom =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv

Tactic:
by
  simp [mapComp'₀₂₃_inv _ _ _ _ _ _ _ h₀₂ h₁₃ hf]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
hf : ∀ a ∈ l, Zigzag a j₂
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }

Tactic:
refine ⟨l.pmap f hf, ?_, by grind⟩

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
hf : ∀ a ∈ l, Zigzag a j₂
⊢ List.IsChain Zag ({ obj := j₁, property := hj₁ } :: List.pmap f l hf)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ W.IsInvertedBy₂ W (curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj L')

Tactic:
by
  rintro ⟨X₁, Y₁⟩ ⟨X₂, Y₂⟩ ⟨f₁, f₂⟩ ⟨hf₁, hf₂⟩
  have := Localization.inverts L' W _ (W.whiskerRight_mem f₁ hf₁ Y₁)
  have := Localization.inverts L' W _ (W.whiskerLeft_mem X₂ f₂ hf₂)
  dsimp
  infer_instance

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ : C
⊢ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom =
    ((μ L W ε X₁ X₂).hom ⊗ₘ 𝟙 (L'.obj X₃)) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ (𝟙 (L'.obj X₁) ⊗ₘ (μ L W ε X₂ X₃).inv)

Tactic:
dsimp +instances [monoidalCategoryStruct, associator]
  simp only [Functor.map_id, comp_id, NatTrans.id_app, id_comp]
  rw [Localization.associator_hom_app_app_app]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: case refine_1
X R : Type w
p₁ p₂ : R ⟶ X
e : TransitiveRelation p₁ p₂
x₁ x₂ x₃ : X
x✝¹ : Rel.ofPair p₁ p₂ x₁ x₂
x✝ : Rel.ofPair p₁ p₂ x₂ x₃
r : R
hr₁ : (ConcreteCategory.hom p₁) r = x₁
hr₂ : (ConcreteCategory.hom p₂) r = x₂
r' : R
hr₁' : (ConcreteCategory.hom p₁) r' = x₂
hr₂' : (ConcreteCategory.hom p₂) r' = x₃
⊢ (ConcreteCategory.hom p₁)
      ((ConcreteCategory.hom e.t) ((PullbackCone.IsLimit.equivPullbackObj e.isLimit).symm ⟨(r, r'), ⋯⟩)) =
    x₁

pp: case refine_2
X R : Type w
p₁ p₂ : R ⟶ X
e : TransitiveRelation p₁ p₂
x₁ x₂ x₃ : X
x✝¹ : Rel.ofPair p₁ p₂ x₁ x₂
x✝ : Rel.ofPair p₁ p₂ x₂ x₃
r : R
hr₁ : (ConcreteCategory.hom p₁) r = x₁
hr₂ : (ConcreteCategory.hom p₂) r = x₂
r' : R
hr₁' : (ConcreteCategory.hom p₁) r' = x₂
hr₂' : (ConcreteCategory.hom p₂) r' = x₃
⊢ (ConcreteCategory.hom p₂)
      ((ConcreteCategory.hom e.t) ((PullbackCone.IsLimit.equivPullbackObj e.isLimit).symm ⟨(r, r'), ⋯⟩)) =
    x₃

Tactic:
all_goals simpa

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

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.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
⊢ ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ

Tactic:
use IsCartesian.map p f φ ψ ≫ φ'.inv

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
⊢ (fun χ ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) (IsCartesian.map p f φ ψ ≫ φ'.inv) ∧
    ∀ (y : c ⟶ a'), (fun χ ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = ψ) y → y = IsCartesian.map p f φ ψ ≫ φ'.inv
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom (f.hom ≫ Y.ρ g⁻¹)) x = (ConcreteCategory.hom (Y.ρ g⁻¹ * Y.ρ g).hom) ↑y

Tactic:
FintypeCat.comp_apply,

Goal state after:
G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom (Y.ρ g⁻¹)) ((ConcreteCategory.hom f.hom) x) = (ConcreteCategory.hom (Y.ρ g⁻¹ * Y.ρ g).hom) ↑y
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t)))
      ((ConcreteCategory.hom (F.map u ≫ F.map (Pi.map' ⇑(fiberPerm h b) fun j ↦ (Iso.refl X).hom))) a)

Tactic:
FintypeCat.comp_apply,

Goal state after:
case convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t)))
      ((ConcreteCategory.hom (F.map (Pi.map' ⇑(fiberPerm h b) fun j ↦ (Iso.refl X).hom)))
        ((ConcreteCategory.hom (F.map u)) a))