mathlib-initiative/mathlib-tactics huggingface dataset:
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.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : P (Abelian.image (z ≫ f))
⊢ P (Abelian.image z)

Tactic:
← exists_comp_monoModSerre_eq_zero_iff P

Goal state after:
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.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : ∃ Y' s, ∃ (_ : P.monoModSerre s), (z ≫ f) ≫ s = 0
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), z ≫ s = 0
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ (𝟙 M).hom = 𝟙 M.V

Tactic:
id_hom

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ 𝟙 M.V = 𝟙 M.V
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ (𝟙 N).hom = 𝟙 N.V

Tactic:
id_hom

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ 𝟙 N.V = 𝟙 N.V
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
⊢ ((ObjectProperty.ι IsContinuous ⋙ Action.res V ↑f).obj X).IsContinuous

Tactic:
by
    constructor
    let v : G × (forget₂ _ TopCat).obj X → H × (forget₂ _ TopCat).obj X := fun p ↦ (f p.1, p.2)
    have : Continuous v := by fun_prop
    let u : H × (forget₂ _ TopCat).obj X → (forget₂ _ TopCat).obj X :=
      fun p ↦ (forget₂ _ TopCat).map (X.obj.ρ p.1) p.2
    have : Continuous u := X.2.1
    change Continuous (u ∘ v)
    fun_prop

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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
⊢ R.IsRightAdjoint

Tactic:
let : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := by
      infer_instance

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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
this : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := inferInstance
⊢ R.IsRightAdjoint
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
      ((preinclusion B).map { as := p } ≫ f✝) ◁ η✝.mk ≫
        (normalizeIso p f✝).hom ▷ h✝ ≫ (normalizeIso (normalizeAux p f✝) h✝).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      eqToHom ⋯

Tactic:
whisker_exchange_assoc,

Goal state after:
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
      (normalizeIso p f✝).hom ▷ g✝ ≫
        (preinclusion B).map { as := normalizeAux p f✝ } ◁ η✝.mk ≫ (normalizeIso (normalizeAux p f✝) h✝).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.whisker_right h η') ≫ (normalizeIso p (Hom.comp g✝ h)).hom =
    (normalizeIso p (Hom.comp f✝ h)).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| whisker_right h η' ih =>

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
a✝ : J
⊢ Nonempty (ConnectedComponents.Component (Quotient.mk'' a✝))

Tactic:
exact ⟨⟨_, rfl⟩⟩

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₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    simp only [tensorObjImpl, Subobject.inf_pullback]
    apply inf_le_inf <;> rw [← Subobject.pullback_comp, ← Subobject.pullback_comp]
    · have := (Subobject.pullback (prod.map π₁ π₁ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le f)
      rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this
      convert! this using 3 <;> simp
    · have := (Subobject.pullback (prod.map π₂ π₂ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le g)
      rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this
      convert! this using 3 <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str

Tactic:
rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ F.map f.f ≫ (adj.homEquiv V₂.V V₂.V).symm V₂.str = (adj.homEquiv V₁.V V₁.V).symm V₁.str ≫ f.f

Tactic:
rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
    f.h]

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
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      (ρ_ ((F₁.obj i ⟶[V] F₂.obj i) ⊗ F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        ((F₁.obj i ⟶[V] F₂.obj i) ⊗ F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫
          (eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ▷ F₃.obj i ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)

Tactic:
whisker_exchange_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
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      (ρ_ ((F₁.obj i ⟶[V] F₂.obj i) ⊗ F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ▷ 𝟙_ V ≫
          (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)
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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      enrichedHom V F₁ F₂ ◁ eId V (F₂.obj j) ≫
        end_.π (diagram V F₁ F₂) j ▷ ((diagram V F₂ F₂).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
whisker_exchange_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
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      end_.π (diagram V F₁ F₂) j ▷ 𝟙_ V ≫
        ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ eId V (F₂.obj j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
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₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
          ((diagram V F₃ F₄).obj (Opposite.op j)).obj j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)

Tactic:
← associator_inv_naturality_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
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₄
j : J
| (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    (α_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j) (((diagram V F₂ F₃).obj (Opposite.op j)).obj j)
          (((diagram V F₃ F₄).obj (Opposite.op j)).obj j)).inv ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
          ((diagram V F₃ F₄).obj (Opposite.op j)).obj j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : HasFibers p
S : 𝒮
a b : Fib p S
φ : a ⟶ b
⊢ p.IsHomLift (𝟙 S) ((ι S).map φ)

Tactic:
by
  apply of_fac p _ _ (proj_eq a) (proj_eq b)
  rw [← Functor.comp_map, Functor.congr_hom (comp_const S)]
  simp

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
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₄
j : J
| enrichedHom V F₁ F₂ ◁ (end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    enrichedHom V F₁ F₂ ◁ eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
      end_.π (diagram V F₁ F₂) j ▷ ((diagram V F₂ F₄).obj (Opposite.op j)).obj j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)

Tactic:
whisker_exchange_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
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₄
j : J
| enrichedHom V F₁ F₂ ◁ (end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    end_.π (diagram V F₁ F₂) j ▷
        (((diagram V F₂ F₃).obj (Opposite.op j)).obj j ⊗ ((diagram V F₃ F₄).obj (Opposite.op j)).obj j) ≫
      ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁
          eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)
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₄
j : J
| enrichedHom V F₁ F₂ ◁ (end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    end_.π (diagram V F₁ F₂) j ▷
        (((diagram V F₂ F₃).obj (Opposite.op j)).obj j ⊗ ((diagram V F₃ F₄).obj (Opposite.op j)).obj j) ≫
      ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁
          eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)

Tactic:
whisker_exchange_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
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₄
j : J
| end_.π (diagram V F₁ F₂) j ▷ (enrichedHom V F₂ F₃ ⊗ enrichedHom V F₃ F₄) ≫
    ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ (end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁
          eComp V (Opposite.unop (F₂.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
⊢ ∃ a, (Fiber.inducedFunctor ⋯).obj a = Y

Tactic:
have hYS : (fiberInclusion.obj Y).base = S := by simpa using! Y.2

Goal state after:
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (fiberInclusion.obj Y).base = S
⊢ ∃ a, (Fiber.inducedFunctor ⋯).obj a = Y
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
α : Type u_4
c : ComplexShape α
K L : HomologicalComplex C c
f : K ⟶ L
⊢ QuasiIso f ↔ ∀ (i : I), QuasiIso (((F i).mapHomologicalComplex c).map f)

Tactic:
by
  simp only [_root_.quasiIso_iff, hP.quasiIsoAt_iff]
  tauto

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)
⊢ (g * h) • x = g • h • x

Tactic:
by
    change J.map (g * h) x = (J.map h ≫ J.map g) x
    rw [← SingleObj.comp_as_mul]
    · simp
      rfl

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

Goal state before:
pp: G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
| J.ColimitTypeRel ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Tactic:
rhs

Goal state after:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
| (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: case h
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) ((ConcreteCategory.hom (X.ρ g⁻¹).hom) x) = ↑y

Tactic:
calc (X.ρ g⁻¹ ≫ f.hom) x
          = ((Y.ρ g⁻¹ * Y.ρ g)).hom y.val := by rw [f.comm, FintypeCat.comp_apply, h]; rfl
        _ = y.val := by
          simp [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_hom]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this✝ : Fintype ↑T
this : MulAction G (FintypeCat.of ↑T).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := FintypeCat.homMk Subtype.val, comm := ⋯ }
⊢ ∃ g, g • x = y

Tactic:
have : Mono i := ConcreteCategory.mono_of_injective _ (Subtype.val_injective)

Goal state after:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this✝¹ : Fintype ↑T
this✝ : MulAction G (FintypeCat.of ↑T).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)
i : T' ⟶ X := { hom := FintypeCat.homMk Subtype.val, comm := ⋯ }
this : Mono i
⊢ ∃ g, g • x = y
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
⊢ s.pt ⟶ WalkingPair.casesOn WalkingPair.right c₁.pt c₂.pt

Tactic:
· exact Fan.IsLimit.lift h₂ (fun a ↦ s.proj (.inr a))

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

Goal state before:
pp: case pos
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
hn2 : Nat.card (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
refine ⟨ι₁ ⊕ ι₂, Sum.elim f₁ f₂,
      Cofan.combPairHoms (Cofan.mk Y g₁) (Cofan.mk Z g₂) (BinaryCofan.mk v u), ?_⟩

Goal state after:
case pos
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
hn2 : Nat.card (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
⊢ ∃ x, (∀ (i : ι₁ ⊕ ι₂), IsConnected (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
⊢ ∀ {c d : D} {p : c ⟶ d}, p ∈ {x | Map.Arrows φ hφ S c d x} → Groupoid.inv p ∈ {x | Map.Arrows φ hφ S d c x}

Tactic:
by
    rintro _ _ _ ⟨⟩
    rw [inv_eq_inv, ← Functor.map_inv, ← inv_eq_inv]
    constructor; apply S.inv; assumption

Goal state after: