mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵖ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      (η.naturality f).hom ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          η.app a ◁ (ι.naturality f).hom ≫ Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv

Tactic:
whisker_exchange_assoc

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵖ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      (η.naturality f).hom ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      (F.map f ≫ η.app b) ◁ Γ.as.app b ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
whisker_exchange_assoc

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      η.naturality f ▷ θ.app b ≫
        (η.app a ≫ G.map f) ◁ Γ.as.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        θ.naturality f ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      η.naturality f ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          η.app a ◁ ι.naturality f ≫ Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv

Tactic:
whisker_exchange_assoc

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        θ.naturality f ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      η.naturality f ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv
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
⊢ rightZigzag t.unit ε = (ρ_ t.extension).hom ≫ (λ_ t.extension).inv

Tactic:
by
      apply (cancel_epi (ρ_ _).inv).mp
      apply H.hom_ext
      calc _
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (t.unit ▷ _ ≫ _ ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 _ := by
          rw [rightZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 _ := by
          rw [← whisker_exchange]; bicategory
        _ = _ := by
          rw [← leftZigzag, Hε]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:

Tactic:
_
        _ = (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = t.unit ▷ (𝟙 c) ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv := by
          rw [Hσ]
          dsimp only [τ]
          bicategory
        _ = _ := by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

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

Tactic:
subst hf h₀₂ h₁₃

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

Goal state before:
pp: case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : ↑s.pt
j : J
⊢ (hom (limit.π (F ⋙ objects) j)) ((limitConeLift F s).toFunctor.obj X) =
    (hom (limit.π (F ⋙ objects) j)) (m.toFunctor.obj X)

Tactic:
simp [← comp_apply, ← w j]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₁₂ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
D₁₂ : Type u_9
D₂₃ : Type u_10
C : Type u_11
D : Type u_12
inst✝²¹ : Category.{v_1, u_1} C₁
inst✝²⁰ : Category.{v_2, u_2} C₂
inst✝¹⁹ : Category.{v_3, u_3} C₃
inst✝¹⁸ : Category.{v_4, u_6} D₁
inst✝¹⁷ : Category.{v_5, u_7} D₂
inst✝¹⁶ : Category.{v_6, u_8} D₃
inst✝¹⁵ : Category.{v_7, u_4} C₁₂
inst✝¹⁴ : Category.{v_8, u_5} C₂₃
inst✝¹³ : Category.{v_9, u_9} D₁₂
inst✝¹² : Category.{v_10, u_10} D₂₃
inst✝¹¹ : Category.{v_11, u_11} C
inst✝¹⁰ : Category.{v_12, u_12} D
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
L₁₂ : C₁₂ ⥤ D₁₂
L₂₃ : C₂₃ ⥤ D₂₃
L : C ⥤ D
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
W₁₂ : MorphismProperty C₁₂
W₂₃ : MorphismProperty C₂₃
inst✝⁹ : W₁.ContainsIdentities
inst✝⁸ : W₂.ContainsIdentities
inst✝⁷ : W₃.ContainsIdentities
inst✝⁶ : L₁.IsLocalization W₁
inst✝⁵ : L₂.IsLocalization W₂
inst✝⁴ : L₃.IsLocalization W₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C
F : C₁ ⥤ C₂₃ ⥤ C
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
iso : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
F₁₂' : D₁ ⥤ D₂ ⥤ D₁₂
G' : D₁₂ ⥤ D₃ ⥤ D
F' : D₁ ⥤ D₂₃ ⥤ D
G₂₃' : D₂ ⥤ D₃ ⥤ D₂₃
inst✝³ : Lifting₂ L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂'
inst✝² : Lifting₂ L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G'
inst✝¹ : Lifting₂ L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F'
inst✝ : Lifting₂ L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ ((G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂').hom.app X₁).app X₂)).app
          (L₃.obj X₃) ≫
        ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G').hom.app ((F₁₂.obj X₁).obj X₂)).app X₃) ≫
      L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
        ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
          (F'.obj (L₁.obj X₁)).map
            (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃').inv.app X₂).app X₃) =
    (G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂').hom.app X₁).app X₂)).app
        (L₃.obj X₃) ≫
      ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G').hom.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫
        L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
            (F'.obj (L₁.obj X₁)).map
              (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃').inv.app X₂).app X₃)

Tactic:
simp only [Category.assoc]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
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₃
⊢ Pentagon Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₄, ⟨e₄⟩⟩ : ∃ X₄, Nonempty ((L').obj X₄ ≅ Y₄) := ⟨_, ⟨(L').objObjPreimageIso Y₄⟩⟩

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
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₄
⊢ Pentagon Y₁ Y₂ Y₃ Y₄
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✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ▷ X = coprod.inr ≫ (∂R X Y Z).hom

Tactic:
coprod_inr_rightDistrib_hom

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ▷ X = coprod.inr ▷ X
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasEnd F
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (F'.obj (op j)).map φ
⊢ (π F j ≫ (f.app (op j)).app j) ≫ (F'.obj (op j)).map φ = (π F j' ≫ (f.app (op j')).app j') ≫ (F'.map φ.op).app j'

Tactic:
simp only [Category.assoc]

Goal state after:
J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasEnd F
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (F'.obj (op j)).map φ
⊢ π F j ≫ (f.app (op j)).app j ≫ (F'.obj (op j)).map φ = π F j' ≫ (f.app (op j')).app j' ≫ (F'.map φ.op).app 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
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ (eHomEquiv V) (τ.app i ≫ F₂.map f) = (eHomEquiv V) (τ.app j) ≫ ((diagram V F₁ F₂).map f.op).app j

Tactic:
dsimp
      simp only [← NatTrans.naturality, eHomEquiv_comp, tensorHom_def', id_whiskerLeft,
        assoc, Iso.inv_hom_id_assoc, eHomWhiskerRight]

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)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    (end_.π (diagram V F₁ F₂) j ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
      ((λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
        (((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
          (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)

Tactic:
leftUnitor_inv_whiskerRight_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)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    (end_.π (diagram V F₁ F₂) j ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
      (λ_ ((F₁.obj j ⟶[V] F₂.obj j) ⊗ F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        (α_ (𝟙_ V) (F₁.obj j ⟶[V] F₂.obj j) (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
          (((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
            (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
              eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
𝒵 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
⊢ F.toFunctor ⋙ 𝒴.p = 𝒳.p

Tactic:
F.w

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
𝒵 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
⊢ 𝒳.p = 𝒳.p
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ (F.toFunctor ⋙ 𝒴.p).obj a = 𝒳.p.obj a

Tactic:
F.w

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ 𝒳.p.obj a = 𝒳.p.obj a
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift g χ'
hφ' : (forget F).IsHomLift (g ≫ f) (χ' ≫ cartesianLift a f)
⊢ g = χ'.base

Tactic:
simpa using IsHomLift.fac (forget F) g χ'

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

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✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Tactic:
haveI : ∀ b, PreservesLimitsOfShape J
      (colim (J := (R ⋙ CostructuredArrow.functor L).obj b) (C := Type u₁)) := fun b => by
    simp only [comp_obj, CostructuredArrow.functor_obj, Cat.of_α]
    exact filtered_colim_preservesFiniteLimits

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✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (colimit F.flip) ⟶ colimit (limit F)
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 : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ Mono S.f

Tactic:
hP.jointlyReflectMonomorphisms.mono_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 : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ ∀ (i : I), Mono ((F i).map S.f)
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : X ⟶ Y
a✝ : Mono (F.map f)
this : IsIso (pullback.fst (F.map f) (F.map f))
⊢ IsIso ((PreservesPullback.iso F f f).hom ≫ pullback.fst (F.map f) (F.map f))

Tactic:
exact IsIso.comp_isIso

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (equalizer.ι (F.map f) (F.map g))
⊢ IsIso (equalizerComparison f g F ≫ equalizer.ι (F.map f) (F.map g))

Tactic:
exact IsIso.comp_isIso

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).obj
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
this : ∃ φ, (ConcreteCategory.hom (F.map φ.hom)) x = g⁻¹ • x
⊢ g • n • g⁻¹ • x = x

Tactic:
obtain ⟨φ, h⟩ := this

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).obj
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
φ : Aut X
h : (ConcreteCategory.hom (F.map φ.hom)) x = g⁻¹ • x
⊢ g • n • g⁻¹ • x = x
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝¹ x✝ : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
Z : C
f : Z ⟶ A ⨯ B
z : (F.obj Z).obj
hgal : IsGalois Z
hfz : (ConcreteCategory.hom (F.map f)) z = (fiberBinaryProductEquiv F A B).symm (a, b)
⊢ (ConcreteCategory.hom (F.map (f ≫ prod.fst))) { obj := Z, pt := z, isGalois := hgal }.pt =
    { obj := A, pt := a, isGalois := isGalois✝¹ }.pt

pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝¹ x✝ : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
Z : C
f : Z ⟶ A ⨯ B
z : (F.obj Z).obj
hgal : IsGalois Z
hfz : (ConcreteCategory.hom (F.map f)) z = (fiberBinaryProductEquiv F A B).symm (a, b)
⊢ (ConcreteCategory.hom (F.map (f ≫ prod.snd))) { obj := Z, pt := z, isGalois := hgal }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt

Tactic:
· simp only [F.map_comp, hfz, FintypeCat.comp_apply, fiberBinaryProductEquiv_symm_fst_apply]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝¹ x✝ : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
Z : C
f : Z ⟶ A ⨯ B
z : (F.obj Z).obj
hgal : IsGalois Z
hfz : (ConcreteCategory.hom (F.map f)) z = (fiberBinaryProductEquiv F A B).symm (a, b)
⊢ (ConcreteCategory.hom (F.map (f ≫ prod.snd))) { obj := Z, pt := z, isGalois := hgal }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 : (ConcreteCategory.hom (F.map i)) y = x
left✝ : IsConnected Y
right✝ : Mono i
⊢ ∃ i xi, x = (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi

Tactic:
obtain ⟨Z, f, z, hgal, hfz⟩ := exists_hom_from_galois_of_fiber F Y y

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 : (ConcreteCategory.hom (F.map i)) y = x
left✝ : IsConnected Y
right✝ : Mono i
Z : C
f : Z ⟶ Y
z : (F.obj Z).obj
hgal : IsGalois Z
hfz : (ConcreteCategory.hom (F.map f)) z = y
⊢ ∃ i xi, x = (ConcreteCategory.hom ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app i)) xi