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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

Tactic:
use pullback.fst (Abelian.factorThruImage S.f) c

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pseudoApply S.f (Quot.mk (PseudoEqual S.X₁) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))) = ⟦b⟧
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
⊢ R'.complex.d m n ≫ φ.hom.f n ≫ f = 0

Tactic:
by simp [← φ.hom.comm_assoc, hf]

Goal state after:
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
X : C
inst✝ : Injective X
⊢ { X₁ := F.obj X, X₂ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 0,
        X₃ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 1,
        f := F.map (𝟙 X),
        g := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).d 0 1,
        zero := ⋯ }.Exact ∧
    Mono (F.map (𝟙 X))

Tactic:
refine ⟨ShortComplex.Splitting.exact ?_, inferInstance⟩

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
X : C
inst✝ : Injective X
⊢ { X₁ := F.obj X, X₂ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 0,
      X₃ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).X 1,
      f := F.map (𝟙 X),
      g := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).d 0 1,
      zero := ⋯ }.Splitting
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x✝ : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (F g).right = g
x : ActionCategory G X
⊢ (F ↑(𝟙 x)).left x.back = 𝟙 ()

Tactic:
dsimp
    rw [F.map_one]
    rfl

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ rightHom.ker
⊢ inl x.left = x

Tactic:
ext <;> simp_all [MonoidHom.mem_ker]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : f ≫ z ≫ t = 0
this : IsIso (L.map t)
⊢ L.map (cokernel.π f) ≫ L.map (cokernel.desc f (z ≫ t) fac) ≫ inv (L.map t) = L.map z ≫ eqToHom ⋯

Tactic:
simp [← L.map_comp_assoc]

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
⊢ η (F.mapAction G) ≫ ε (F.mapAction G) = 𝟙 ((F.mapAction G).obj (𝟙_ (Action V G)))

Tactic:
by ext; dsimp; rw [η_ε]

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

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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ ⟨(adj₁.homEquiv (U.obj X) (R.obj Y')).symm
        ((adj₂.homEquiv (U.obj X) Y')
          ↑((Cofork.IsColimit.homIso
                (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y')
              (h ≫ g))),
      ⋯⟩ =
    (Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y'))
      ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
          ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
              ((adj₂.homEquiv (U.obj X) Y)
                ↑((Cofork.IsColimit.homIso
                      (colimit.isColimit
                        (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                      Y)
                    h)),
            ⋯⟩ ≫
        R.map g)

Tactic:
Subtype.ext_iff

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

Tactic:
Subtype.ext_iff

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'))
          ((adj₁.homEquiv (L.obj X) (F.obj Y')).symm
            ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h))),
        ⋯⟩ =
    ↑((Fork.IsLimit.homIso
          (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) X)
        (g ≫
          (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'))
                ((adj₁.homEquiv (L.obj Y) (F.obj Y')).symm
                  ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h)),
              ⋯⟩))
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
⊢ (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).hom =
    (eqToHomTransIso e₁ e₂).inv ▷ eqToHom e₃ ≫
      (eqToHomTransIso ⋯ e₃).inv ≫ (eqToHomTransIso e₁ ⋯).hom ≫ eqToHom e₁ ◁ (eqToHomTransIso e₂ e₃).hom

Tactic:
by
  subst_vars
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
⊢ (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).inv =
    eqToHom e₁ ◁ (eqToHomTransIso e₂ e₃).inv ≫
      (eqToHomTransIso e₁ ⋯).inv ≫ (eqToHomTransIso ⋯ e₃).hom ≫ (eqToHomTransIso e₁ e₂).hom ▷ eqToHom e₃

Tactic:
by
  subst_vars
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (α_ f g h).hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯

Tactic:
by
  subst_vars
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (α_ f g h).inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯

Tactic:
by
  subst_vars
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a b c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ η.naturality (f ≫ g) ▷ h ≫ (α_ (η.app a) (G.map (f ≫ g)) h).hom ≫ η.app a ◁ G.mapComp f g ▷ h =
    F.mapComp f g ▷ η.app c ▷ h ≫
      (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫
        (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫
          F.map f ◁ η.naturality g ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                η.naturality f ▷ G.map g ▷ h ≫
                  (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom

Tactic:
by
  rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_comp]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
          η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
X✝ Y✝ Z✝ : Cat
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾(x✝¹ ≫ x✝).toFunctor.mapConnectedComponents =
    ↾x✝¹.toFunctor.mapConnectedComponents ≫ ↾x✝.toFunctor.mapConnectedComponents

Tactic:
by ext x; simpa using (Quotient.exists_rep x).elim (fun _ h => by subst h; rfl)

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
x✝ : ∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩
w : Y✝
hw : w ∈ f a
h : ⟨some b, hb⟩ = ⟨some w, ⋯⟩
⊢ some b = (partialFunToPointed.map f).toFun (some a)

Tactic:
Subtype.ext_iff

Goal state after:
case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
x✝ : ∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩
w : Y✝
hw : w ∈ f a
h : ↑⟨some b, hb⟩ = ↑⟨some w, ⋯⟩
⊢ some b = (partialFunToPointed.map f).toFun (some a)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case refine_1
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ Y₁ ◁ (α_ Y₂ Y₃ Y₄).hom =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
          (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
            L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)

pp: case refine_2
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫
          (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom

Tactic:
· rw [← id_tensorHom, ← id_tensorHom, ← tensorHom_id, ← tensorHom_id, assoc, assoc,
        ← tensor_comp, ← associator_naturality, id_comp, ← comp_id e₁.hom,
        tensor_comp, ← associator_naturality_assoc, ← comp_id (𝟙 ((L').obj X₄)),
        ← tensor_comp_assoc, associator_naturality, comp_id, comp_id,
        ← tensor_comp_assoc, assoc, e₄.inv_hom_id, ← tensor_comp, e₁.inv_hom_id,
        ← tensor_comp, e₂.inv_hom_id, e₃.inv_hom_id, id_tensorHom_id, id_tensorHom_id, comp_id]

Goal state after:
case refine_2
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫
          (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A✝ A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
A : Algebra F
h : Limits.IsInitial A
⊢ (F.map (strInv h) ≫ F.map A.str) ≫ A.str = (A.str ≫ strInv h) ≫ A.str

Tactic:
strInv,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A✝ A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
A : Algebra F
h : Limits.IsInitial A
⊢ (F.map (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ F.map A.str) ≫ A.str =
    (A.str ≫ (h.to { a := F.obj A.a, str := F.map A.str }).f) ≫ A.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)

Tactic:
strInv,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ A.str ≫ (h.to { a := F.obj A.a, str := F.map A.str }).f = 𝟙 (F.obj A.a)
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ F.map A.str ≫ F.map (strInv h) = A.str ≫ strInv h ≫ A.str

Tactic:
strInv,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ F.map A.str ≫ F.map (h.from { V := F.obj A.V, str := F.map A.str }).f =
    A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f ≫ A.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ strInv h ≫ A.str = 𝟙 (F.obj A.V)

Tactic:
strInv,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ (h.from { V := F.obj A.V, str := F.map A.str }).f ≫ A.str = 𝟙 (F.obj A.V)
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₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
⊢ (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
      enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄ =
    enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄

Tactic:
ext j
  conv_lhs =>
    rw [assoc, assoc, enrichedComp_π,
      tensorHom_def_assoc, ← comp_whiskerRight_assoc, enrichedComp_π,
      comp_whiskerRight_assoc, ← whisker_exchange_assoc,
      ← whisker_exchange_assoc, ← tensorHom_def'_assoc, ← associator_inv_naturality_assoc]
  conv_rhs =>
    rw [assoc, enrichedComp_π, tensorHom_def'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
      enrichedComp_π, MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange_assoc,
      whisker_exchange_assoc, ← tensorHom_def_assoc]
  dsimp
  rw [e_assoc]

Goal state after:
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
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerLeft V (F₁.obj (G.obj i)) (F₂.map (G.map f)) ≫
        eHomWhiskerLeft V (F₁.obj (G.obj i)) (e₂.hom.app j) ≫ eHomWhiskerRight V (e₁.inv.app i) (F₂'.obj j) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j) ≫ eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)

Tactic:
enrichedHom_condition_assoc,

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
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (F₁.map (G.map f)) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁.obj (G.obj i)) (e₂.hom.app j) ≫ eHomWhiskerRight V (e₁.inv.app i) (F₂'.obj j) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j) ≫ eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)

Tactic:
← IsIso.inv_hom_id (p.map φ)

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (CategoryTheory.inv (p.map φ) ≫ p.map φ) (φ' ≫ φ)
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
⊢ IsLimit c

Tactic:
by
  suffices IsIso (limit.lift _ c) from
    IsLimit.ofIsoLimit (limit.isLimit _)
      (Cone.ext (asIso (limit.lift _ c) :)).symm
  rw [hF.isIso_iff]
  intro i
  let H := isLimitOfPreserves (F i) (limit.isLimit G)
  let e := IsLimit.conePointUniqueUpToIso (hc i) H
  have : e.hom = (F i).map (limit.lift G c) :=
    H.hom_ext (fun j ↦ by
      simpa [← Functor.map_comp] using
        IsLimit.conePointUniqueUpToIso_hom_comp (hc i) H j)
  rw [← this]
  infer_instance

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

Goal state before:
pp: M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ (ConcreteCategory.hom (J.map (g * h))) x = (ConcreteCategory.hom (J.map h ≫ J.map g)) x

Tactic:
rw [← SingleObj.comp_as_mul]

Goal state after:
M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ (ConcreteCategory.hom (J.map (h ≫ g))) x = (ConcreteCategory.hom (J.map h ≫ J.map g)) x

case y
M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ SingleObj M
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: X Y : FintypeCat
f : X ⟶ Y
⊢ FintypeCat

Tactic:
haveI : Fintype (↑(Set.range f)ᶜ) := Fintype.ofFinite _
  exact FintypeCat.of (↑(Set.range f)ᶜ)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
let F := GaloisCategory.getFiberFunctor C
  exact has_decomp_connected_components_aux F (Nat.card <| F.obj X) X rfl

Goal state after: