mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a)

Tactic:
rw [η.naturality_id]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.app a ◁ G.mapId a ≫ (ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv) ▷ θ.app a ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ c =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (f ≫ g) ⊗≫
          (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
          (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
          ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
            F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))

Tactic:
rw [η.naturality_id]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      ((λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv ≫ η.app a ◁ G.mapId a) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
Module: Mathlib.CategoryTheory.Category.PartialFun

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

Tactic:
by classical exact Equiv.optionSubtypeNe X.point

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
⊢ IsIso (colimit.pre G L)

Tactic:
have : ∀ (b : B), Final ((whiskerLeft R (preFunctor L (𝟭 T))).app b).toFunctor := fun b =>
    inferInstanceAs (Final (CostructuredArrow.toOver L (R.obj b)))

Goal state after:
A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
this : ∀ (b : B), ((R.whiskerLeft (preFunctor L (𝟭 T))).app b).toFunctor.Final
⊢ IsIso (colimit.pre G L)
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y Z : limit (F ⋙ objects)
f : limit (homDiagram X Y)
g : limit (homDiagram Y Z)
j j' : J
h : j ⟶ j'
⊢ (hom ((homDiagram X Z).map h)) ((hom (limit.π (homDiagram X Y) j)) f ≫ (hom (limit.π (homDiagram Y Z) j)) g) =
    (hom (limit.π (homDiagram X Y) j')) f ≫ (hom (limit.π (homDiagram Y Z) j')) g

Tactic:
simp [-homDiagram_obj, ← limit.w_apply (homDiagram X Y) h f,
      ← limit.w_apply (homDiagram Y Z) h g]

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : ↑s.pt
f : X ⟶ Y
⊢ (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.map f = eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯

Tactic:
by
      dsimp [limitConeLift]
      exact Types.Limit.π_mk.{v, v} _ _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
X✝ Y✝ : C₂
⊢ ∀ (f : X✝ ⟶ Y✝), W₂ f → IsIso ((prodLift₁ F hF).flip.map f)

Tactic:
f₂

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
X✝ Y✝ : C₂
f₂ : X✝ ⟶ Y✝
⊢ W₂ f₂ → IsIso ((prodLift₁ F hF).flip.map f₂)
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.as = Y✝.1.as
f₂ : X✝.2.as = Y✝.2.as
⊢ { as := (Y✝.1.as, X✝.2.as) } = { as := (Y✝.1.as, Y✝.2.as) }

Tactic:
f₂

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
⊢ { as := (Y✝.1.as, Y✝.2.as) } = { as := (Y✝.1.as, Y✝.2.as) }
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
⊢ (((Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
                    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)).hom.app
              (L'.obj X₁)).app
          (L'.obj X₂)).app
      (L'.obj X₃) =
    (((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
        ((tensorBifunctor L W ε).obj (L'.obj (X₁ ⊗ X₂))).map (𝟙 (L'.obj X₃))) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫
            ((tensorBifunctor L W ε).map (𝟙 (L'.obj X₁))).app (L'.obj (X₂ ⊗ X₃)) ≫
              ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv

Tactic:
simp only [Functor.map_id, comp_id, NatTrans.id_app, id_comp]

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
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
⊢ (((Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
                    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)).hom.app
              (L'.obj X₁)).app
          (L'.obj X₂)).app
      (L'.obj X₃) =
    ((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : BraidedCategory C
X Y Z : C
⊢ coprodComparison (tensorLeft X) Y Z ≫ (β_ X (Y ⨿ Z)).hom =
    coprod.map (β_ X Y).hom (β_ X Z).hom ≫ coprodComparison (tensorRight X) Y Z

Tactic:
simp [coprodComparison]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : SymmetricCategory C
X Y Z : C
⊢ coprodComparison (tensorRight X) Y Z ≫ (β_ (Y ⨿ Z) X).hom =
    coprod.map (β_ Y X).hom (β_ Z X).hom ≫ coprodComparison (tensorLeft X) Y Z

Tactic:
simp [coprodComparison]

Goal state after:
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
inst✝ : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
| f

Tactic:
← id_comp f

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : HasFibers p
inst✝ : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
| 𝟙 R ≫ f
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ 𝟙 (G'.obj (L₁.obj X₁)) ≫
      G'.map (η.app (L₁.obj X₁)) ≫ 𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁

Tactic:
Category.id_comp,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (η.app (L₁.obj X₁)) ≫ 𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (η.app (L₁.obj X₁)) ≫ 𝟙 (G'.obj (F'.obj (G'.obj (L₁.obj X₁)))) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ =
    𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁

Tactic:
Category.id_comp,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (η.app (L₁.obj X₁)) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ = 𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (η.app (L₁.obj X₁)) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ = 𝟙 (G'.obj (L₁.obj X₁)) ≫ α.app X₁

Tactic:
Category.id_comp,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (η.app (L₁.obj X₁)) ≫ ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁ = α.app X₁
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ β.app X₂ ≫
      𝟙 (F'.obj (L₂.obj X₂)) ≫
        η.app (F'.obj (L₂.obj X₂)) ≫ 𝟙 (F'.obj (G'.obj (F'.obj (L₂.obj X₂)))) ≫ F'.map (ε.app (L₂.obj X₂)) =
    β.app X₂

Tactic:
Category.id_comp,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) ≫ 𝟙 (F'.obj (G'.obj (F'.obj (L₂.obj X₂)))) ≫ F'.map (ε.app (L₂.obj X₂)) =
    β.app X₂
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) ≫ 𝟙 (F'.obj (G'.obj (F'.obj (L₂.obj X₂)))) ≫ F'.map (ε.app (L₂.obj X₂)) =
    β.app X₂

Tactic:
Category.id_comp,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) = β.app X₂
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ Function.Injective ⇑(autEmbedding F)

Tactic:
intro σ τ h

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
⊢ σ = τ