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

Goal state before:
pp: J : Type
inst✝ : SmallCategory J
K : J ⥤ FintypeCat
j : J
⊢ Finite ((K ⋙ FintypeCat.incl).obj j)

Tactic:
by
  simp only [comp_obj, FintypeCat.incl_obj]
  infer_instance

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 : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ (ConcreteCategory.hom (F.map fi2.inv)) ((ConcreteCategory.hom (F.map fi1.hom)) x) = y

Tactic:
rw [hfi1, ← hfi2]

Goal state after:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ (ConcreteCategory.hom (F.map fi2.inv)) ((ConcreteCategory.hom (F.map fi2.hom)) y) = y
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
⊢ (endEquivAutGalois F) (g ≫ f) = (endEquivAutGalois F) g * (endEquivAutGalois F) f

Tactic:
refine AutGalois.ext F (fun A ↦ evaluation_aut_injective_of_isConnected F A A.pt ?_)

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (fun f ↦ (ConcreteCategory.hom (F.map f.hom)) A.pt) ((AutGalois.π F A) ((endEquivAutGalois F) (g ≫ f))) =
    (fun f ↦ (ConcreteCategory.hom (F.map f.hom)) A.pt)
      ((AutGalois.π F A) ((endEquivAutGalois F) g * (endEquivAutGalois F) f))
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ S ∈ 𝓝 1 ↔ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

Tactic:
rw [mem_nhds_iff]
    refine ⟨?_, ?_⟩
    · intro ⟨U, hU, hUopen, hUone⟩
      obtain ⟨I, _, hc, hmem⟩ := exists_set_ker_evaluation_subset_of_isOpen F hUone hUopen
      let P : C := ∏ᶜ fun X : I ↦ X.val
      obtain ⟨A, a, hgal, hbij⟩ := exists_galois_representative F P
      refine ⟨⟨A, a, hgal⟩, trivial, ?_⟩
      intro t (ht : t.hom.app A a = a)
      apply hU
      apply hmem
      have (X : I) : IsConnected X.val := hc X.val X.property
      have (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X
      intro X
      ext x
      simp only [FintypeCat.id_apply]
      obtain ⟨z, rfl⟩ :=
        surjective_of_nonempty_fiber_of_isConnected F (Pi.π (fun X : I ↦ X.val) X) x
      obtain ⟨f, rfl⟩ := hbij.surjective z
      rw [NatTrans.naturality_apply, NatTrans.naturality_apply, ht]
    · intro ⟨X, _, h⟩
      exact ⟨MulAction.stabilizer (Aut F) X.pt, h, stabilizer_isOpen (Aut F) X.pt,
        Subgroup.one_mem _⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f ≫ inv g ≫ g = f ≫ inv f ≫ g

Tactic:
congr 1
                            simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
r : homRel C f g
this :
  ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g

Tactic:
induction r

Goal state after:
case map_id
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
this :
  ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f
X✝ : C
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map ((Quiver.FreeGroupoid.of C).map (𝟙 X✝)) =
    (Quiver.FreeGroupoid.lift φ.toPrefunctor).map (𝟙 ((Quiver.FreeGroupoid.of C).obj X✝))

case map_comp
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
this :
  ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map ((Quiver.FreeGroupoid.of C).map (f✝ ≫ g✝)) =
    (Quiver.FreeGroupoid.lift φ.toPrefunctor).map
      ((Quiver.FreeGroupoid.of C).map f✝ ≫ (Quiver.FreeGroupoid.of C).map g✝)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G✝ : Type u₁
inst✝ : Groupoid G✝
F G : FreeGroupoid C ⥤ G✝
h : of C ⋙ F = of C ⋙ G
⊢ F = G

Tactic:
rw [lift_unique (of C ⋙ G) F h, ← lift_unique (of C ⋙ G) G rfl]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ (∀ ⦃x : (c : C) × (d : C) × (c ⟶ d)⦄, x ∈ S → x ∈ T) ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
Sigma.forall

Goal state after:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ (∀ (a : C) (b : (d : C) × (a ⟶ d)), ⟨a, b⟩ ∈ S → ⟨a, b⟩ ∈ T) ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
i : IsInitial K
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom (t.from X) ↔ HasLiftingProperty f (t.from (L ⟹ X))

Tactic:
by
  rw [hasLiftingProperty_mk_isInitial_iff']
  exact HasLiftingProperty.iff_of_arrow_iso_right f
    (Arrow.isoMk' _ _ (Iso.refl _) ((IsTerminal.isTerminalObj (ihom L) _ t).uniqueUpToIso t)
      (t.hom_ext _ _))

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F : A ⥤ B
G H : B ⥤ C
η : G ⟶ H
x✝ : A
⊢ ((inclLeft A D).whiskerLeft (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))).app x✝ =
    ((inclLeft A D).whiskerLeft
          ((mapCompLeft D F G).hom ≫
            (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F H).inv)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F : A ⥤ B
G H : B ⥤ C
η : G ⟶ H
x✝ : D
⊢ ((inclRight A D).whiskerLeft (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))).app x✝ =
    ((inclRight A D).whiskerLeft
          ((mapCompLeft D F G).hom ≫
            (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F H).inv)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F G : A ⥤ B
η : F ⟶ G
H : B ⥤ C
x✝ : A
⊢ ((inclLeft A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclLeft A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
inst✝¹ : Category.{v_3, u_3} C
inst✝ : Category.{v_4, u_4} D
F G : A ⥤ B
η : F ⟶ G
H : B ⥤ C
x✝ : D
⊢ ((inclRight A D).whiskerLeft (mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D))).app x✝ =
    ((inclRight A D).whiskerLeft
          ((mapCompLeft D F H).hom ≫
            Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
x✝ : A
⊢ ((inclLeft A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclLeft A E).whiskerLeft
          ((mapCompLeft E (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
              ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
                (mapPair F (𝟭 E)).whiskerLeft (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
E : Type u_5
inst✝ : Category.{v_5, u_5} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
x✝ : E
⊢ ((inclRight A E).whiskerLeft (mapWhiskerRight (F.associator G H).hom (𝟭 E))).app x✝ =
    ((inclRight A E).whiskerLeft
          ((mapCompLeft E (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
              ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
                (mapPair F (𝟭 E)).whiskerLeft (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C (𝟭 A) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : A
⊢ ((inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclLeft A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
x✝ : C
⊢ ((inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C))).app x✝ =
    ((inclRight A C).whiskerLeft
          ((mapCompLeft C F (𝟭 B)).hom ≫
            (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)).app
      x✝

Tactic:
simp [mapCompLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η ▷ h).toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor h.toFunctor)).hom ≫
        NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η.toNatTrans) ▷ (mapPair (𝟭 C) h.toFunctor).toCatHom ≫
          (Cat.Hom.isoMk (mapCompRight C g.toFunctor h.toFunctor)).inv

Tactic:
by intros; exact congr($(mapWhiskerLeft_whiskerRight C _ _).toCatHom₂)

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

Goal state before:
pp: case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
⊢ (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)

Tactic:
let L₁ := fun j => (L₂ (e j))

Goal state after:
case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
⊢ (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_empty
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst✝³ : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
x✝³ x✝² : (i : PEmpty.{w + 1}) → C i
x✝¹ : x✝³ ⟶ x✝²
x✝ : MorphismProperty.pi W x✝¹
⊢ IsIso x✝¹

Tactic:
isIso_pi_iff

Goal state after:
case h_empty
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst✝³ : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
x✝³ x✝² : (i : PEmpty.{w + 1}) → C i
x✝¹ : x✝³ ⟶ x✝²
x✝ : MorphismProperty.pi W x✝¹
⊢ ∀ (i : PEmpty.{w + 1}), IsIso (x✝¹ i)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case tensorHom_comp_tensorHom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₁✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₁✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((f₁✝.tensor f₂✝).comp (g₁✝.tensor g₂✝)) = projectMapAux f✝ ((f₁✝.comp g₁✝).tensor (f₂✝.comp g₂✝))

Tactic:
dsimp only [projectMapAux]; rw [MonoidalCategory.tensorHom_comp_tensorHom]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
w₃ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c))) =
    ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d))) (R.obj c)).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)))) ∘
        ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c))
w₄ :
  (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj (Opposite.op d)).map (adj.unit.app ((ihom d').obj (R.obj c))) =
    (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
f : (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
this : f = R.map (R.preimage f)
⊢ R.map (L.map (adj.unit.app d)) ≫
      R.map (L.map (R.map (R.preimage f))) ≫ R.map (adj.counit.app (L.obj ((ihom d').obj (R.obj c)))) =
    R.map (R.preimage f)

Tactic:
simp [← map_comp, -map_preimage]

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

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷ T.X ≫ actLeft P Q ▷ T.X

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actRight P Q

Tactic:
rw [← comp_whiskerRight, whiskerLeft_π_actLeft, comp_whiskerRight,
    comp_whiskerRight]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X P.X Q.X).inv ▷ T.X ≫
    P.actLeft ▷ Q.X ▷ T.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actRight P Q
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
rw [← cancel_mono (hT.from A)]
  apply hT.hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
hasDayConvolution : ∀ (F G : C ⥤ V), (tensor C).HasPointwiseLeftKanExtension (F ⊠ G)
hasDayConvolutionUnit : (Functor.fromPUnit (𝟙_ C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (𝟙_ V))
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
F G : C ⊛⥤ V
x y : C
⊢ Limits.colimit.ι (CostructuredArrow.proj (tensor C) (x ⊗ y) ⋙ F.functor ⊠ G.functor)
        (CostructuredArrow.mk (𝟙 (x ⊗ y))) ≫
      (F.isoPointwiseLeftKanExtension G).inv.app (x ⊗ y) =
    (F.η G).app (x, y)

Tactic:
simp [η, isoPointwiseLeftKanExtension]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫ (α_ A A A).inv ▷ A ≫ μ ▷ A ▷ A ≫ (((α_ A A A).hom ≫ 𝒮 ▷ (A ⊗ A)) ≫ A ◁ μ) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 9 10 =>
    rw [← whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫ (α_ A A A).inv ▷ A ≫ μ ▷ A ▷ A ≫ (α_ A A A).hom ≫ (A ◁ μ ≫ 𝒮 ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η