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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
⊢ IsIndObject (limit (F ⋙ (Functor.whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda ⋙ colim))

Tactic:
let G : J ⥤ I ⥤ (Cᵒᵖ ⥤ Type v) := F ⋙ (Functor.whiskeringRight _ _ _).obj yoneda
  apply IsIndObject.map (HasLimit.isoOfNatIso (colimitFlipIsoCompColim G)).hom
  apply IsIndObject.map (colimitLimitIso G).hom
  apply isIndObject_colimit
  exact fun i => IsIndObject.map (limitObjIsoLimitCompEvaluation _ _).inv (hF i)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt (ofCocomplex Z) (n + 1)

Tactic:
by
  rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]
  simp only [HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ofCocomplex,
    CochainComplex.mk', CochainComplex.mk, CochainComplex.of_d]
  match n with
  | 0 => apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)
  | n + 1 => apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n + 1)).f)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
this : ⟦Over.mk (a.hom ≫ f)⟧ = ⟦Over.mk (a'.hom ≫ f)⟧
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ (p ≫ a.hom) ≫ f = (q ≫ a'.hom) ≫ f

Tactic:
by
    simp only [Category.assoc]
    exact comm

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

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

Tactic:
exact ⟨_, kernel.ι f, P.prop_of_iso (Abelian.coimageIsoImage f).symm hf, by simp⟩

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.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
W : C
s : Y ⟶ W
hs : P.monoModSerre s
eq : (z ≫ f) ≫ s = 0
⊢ z ≫ f ≫ s = 0

Tactic:
simpa using! eq

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.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
⊢ z = 0

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (z ≫ (L.objObjPreimageIso W).inv)

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 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ z = 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
⊢ ∀ (x y : R) (b : F ⟶ G), (x * y) • b = x • y • b

Tactic:
intros
        ext
        apply mul_smul

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

Goal state before:
pp: case refine_2
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ (whiskeringLeft L P E).essImage F

Tactic:
· refine ⟨⟨Localization.lift F.obj hF L, ?_⟩,
      ⟨ObjectProperty.isoMk _ (Localization.fac F.obj hF L)⟩⟩
    rw [← exactFunctor_comp_iff L P]
    exact ObjectProperty.prop_of_iso _ (Localization.fac F.obj hF L).symm F.property

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ PreservesColimitsOfShape J H ↔ PreservesColimitsOfShape J (F ⋙ H)

Tactic:
have := adj.isLeftAdjoint

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
⊢ PreservesColimitsOfShape J H ↔ PreservesColimitsOfShape J (F ⋙ H)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
H : D ⥤ E
inst✝² : HasColimitsOfSize.{v, u, v₁, u₁} C
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)

Tactic:
have := adj.isLeftAdjoint

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
H : D ⥤ E
inst✝² : HasColimitsOfSize.{v, u, v₁, u₁} C
inst✝¹ : G.Full
inst✝ : G.Faithful
this : F.IsLeftAdjoint
⊢ PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)
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✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : G
⊢ (leftRegular G ⊗ X).ρ x✝ ≫
      { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom =
    { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom ≫
      (leftRegular G ⊗ trivial G X.V).ρ x✝

Tactic:
ext _

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝¹ : G
x✝ : (leftRegular G ⊗ X).V
⊢ (ConcreteCategory.hom
          ((leftRegular G ⊗ X).ρ x✝¹ ≫
            { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
                  invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯,
                  right_inv := ⋯ }.toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
                  invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯,
                  right_inv := ⋯ }.toIso.hom ≫
            (leftRegular G ⊗ trivial G X.V).ρ x✝¹)).toFun
      x✝
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    t.adj₁.counit.app (H.obj X) ≫ (whiskerRight t.adj₁.unit H).app X

Tactic:
refine Eq.trans ?_ (t.adj₁.counit_naturality <| (whiskerRight t.adj₁.unit H).app X)

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map (G.map ((whiskerRight t.adj₁.unit H).app X)) ≫ t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)

Tactic:
← leftZigzag,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)
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 : (f a).toOption = some w
h : some b = some w
⊢ some w = (partialFunToPointed.map f).toFun (some a)

Tactic:
exact hw.symm

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

Goal state before:
pp: X : Pointed
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X ≃ ((𝟭 Pointed).obj X).X

Tactic:
classical exact Equiv.optionSubtypeNe X.point

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ :
  ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a' h
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Tactic:
obtain ⟨h₃, h₄⟩ := h₃

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: J : Type u_1
K : Type u_2
X✝ Y✝ : Discrete J × Discrete K
x✝ : X✝ ⟶ Y✝
f₁ : X✝.1 ⟶ Y✝.1
f₂ : X✝.2 ⟶ Y✝.2
⊢ (match X✝ with
    | (x, y) => { as := (x.as, y.as) }) =
    match Y✝ with
    | (x, y) => { as := (x.as, y.as) }

Tactic:
discrete_cases

Goal state after:
J : Type u_1
K : Type u_2
X✝ Y✝ : Discrete J × Discrete K
x✝ : X✝ ⟶ Y✝
f₁ : X✝.1.as = Y✝.1.as
f₂ : X✝.2.as = Y✝.2.as
⊢ (match X✝ with
    | (x, y) => { as := (x.as, y.as) }) =
    match Y✝ with
    | (x, y) => { as := (x.as, y.as) }
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (β_ ((Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ⊗ Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
            (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
        (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁
            (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁ comp (Opposite.unop x✝¹) (Opposite.unop x✝²) (Opposite.unop x✝³) ≫
            comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
      (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁ comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ≫
        (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)

Tactic:
rw [← EnrichedCategory.assoc]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (β_ ((Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ⊗ Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
            (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
        (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁
            (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
          (α_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
                (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³)).inv ≫
            (comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ▷
                Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ≫
              comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
      (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁ comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ≫
        (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (homEquiv V) (f ≫ g) = (λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃

Tactic:
by
  ext j
  simp only [homEquiv_apply_π, NatTrans.comp_app, eHomEquiv_comp, assoc,
    enrichedComp_π, Functor.op_obj, tensorHom_comp_tensorHom_assoc]

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

Goal state before:
pp: 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.IsHomLift f φ.hom
a' : 𝒳
g : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (g ≫ f) τ
⊢ (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) (τ ≫ φ.inv)

Tactic:
simpa using (IsHomLift.comp p (g ≫ f) (isoOfIsoLift p f φ).inv τ φ.inv)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
X : C
inst✝ : F.HasPointwiseLeftDerivedFunctorAt W X
⊢ L.HasPointwiseRightKanExtensionAt F (L.obj X)

Tactic:
← hasPointwiseLeftDerivedFunctorAt_iff F L W

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
X : C
inst✝ : F.HasPointwiseLeftDerivedFunctorAt W X
⊢ F.HasPointwiseLeftDerivedFunctorAt W X
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✝³ : HasZeroMorphisms C
inst✝² : (i : I) → HasZeroMorphisms (D i)
inst✝¹ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝ : HasZeroObject C
X : C
hX : ∀ (i : I), IsZero ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ IsIso φ

Tactic:
rw [hP.isIso_iff]

Goal state after:
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✝³ : HasZeroMorphisms C
inst✝² : (i : I) → HasZeroMorphisms (D i)
inst✝¹ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝ : HasZeroObject C
X : C
hX : ∀ (i : I), IsZero ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ ∀ (i : I), IsIso ((F i).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 : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst✝¹ : HasColimit G
inst✝ : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
⊢ IsIso ((F i).map (colimit.desc G c))

Tactic:
let e := IsColimit.coconePointUniqueUpToIso H (hc i)

Goal state after:
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 : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst✝¹ : HasColimit G
inst✝ : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
⊢ IsIso ((F i).map (colimit.desc G c))
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)
S₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
hf : ∀ (i : I), IsIso (ShortComplex.homologyMap ((F i).mapShortComplex.map f))
⊢ IsIso (ShortComplex.homologyMap f)

Tactic:
rw [hP.isIso_iff]

Goal state after:
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)
S₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
hf : ∀ (i : I), IsIso (ShortComplex.homologyMap ((F i).mapShortComplex.map f))
⊢ ∀ (i : I), IsIso ((F i).map (ShortComplex.homologyMap f))
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ

Tactic:
let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  apply evaluation_aut_injective_of_isConnected F (B : C) (F.map f a)
  simp [Aut.Aut_mul_def]

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

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
hu : (ConcreteCategory.hom (G.map u)) y = a
⊢ (ConcreteCategory.hom (F.map ((asIso u).symm ≪≫ asIso v).hom)) a = b

Tactic:
have hv : G.map v y = b := fiberPullbackEquiv_symm_snd_apply _ _ _ h

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
hu : (ConcreteCategory.hom (G.map u)) y = a
hv : (ConcreteCategory.hom (G.map v)) y = b
⊢ (ConcreteCategory.hom (F.map ((asIso u).symm ≪≫ asIso v).hom)) a = b
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (q.cons f ≫ (reverse f).toPath.comp q.reverse) (q ≫ q.reverse)

Tactic:
apply EqvGen.symm

Goal state after:
case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)