mathlib-initiative/mathlib-tactics huggingface dataset:
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' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app j =
    s.π.app j

Tactic:
by
    refine Localization.induction_structuredArrow L W _ (by simp)
      (fun X₁ X₂ f φ hφ ↦ ?_) (fun X₁ X₂ w hw φ hφ ↦ ?_) j
    · have eq := s.π.naturality
        (StructuredArrow.homMk f : StructuredArrow.mk φ ⟶ StructuredArrow.mk (φ ≫ L.map f))
      dsimp at eq hφ ⊢
      rw [id_comp] at eq
      rw [assoc] at hφ
      simp [eq, ← reassoc_of% hφ, ← e.inv.naturality f]
    · have : IsIso (F.map w) := by
        have := Localization.inverts L W w hw
        rw [← NatIso.naturality_2 e w]
        dsimp
        infer_instance
      have eq := s.π.naturality (StructuredArrow.homMk w :
          StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv) ⟶
            StructuredArrow.mk φ)
      dsimp at eq hφ ⊢
      rw [id_comp] at eq
      rw [assoc] at hφ
      simp only [← cancel_mono (F.map w), ← eq, comp_obj, comp_map, assoc,
        ← hφ, ← NatTrans.naturality, ← G.map_comp_assoc,
        Localization.isoOfHom_inv_hom_id, comp_id]

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✝ : IsConnected X
⊢ Nonempty (Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)) ↔
    MulAction.IsPretransitive (Aut X) (F.obj X).obj

Tactic:
exact (MulAction.pretransitive_iff_unique_quotient_of_nonempty (Aut X) (F.obj X)).symm

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ (σ : Aut F), (∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U

Tactic:
refine fun σ h ↦ ha (fun X XinI ↦ ?_)
    suffices h : autEmbedding F σ X = 1 by
      rw [h]
      exact (ho X XinI).right
    have h : σ.hom.app X = 𝟙 (F.obj X) := by
      have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
      ext x
      obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ := Limits.FintypeCat.jointly_surjective
        (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _ (Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x
      rw [FintypeCat.id_apply, ← ha, NatTrans.naturality_apply]
      simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]
    exact Iso.ext h

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
⊢ (toAut F G).ker = ⊥

Tactic:
eq_bot_iff

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
⊢ (toAut F G).ker ≤ ⊥
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂)) (ιTensorObj X Z i₁ i₃ (i₁ + i₃) ⋯) ≫
        MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂))
            (tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i (i₁ + i₃) ⋯) ≫
          ιTensorObj Y (tensorObj Z X) i₂ (i₁ + i₃) k ⋯

Tactic:
← MonoidalCategory.id_tensor_comp_assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂))
          (ιTensorObj X Z i₁ i₃ (i₁ + i₃) ⋯ ≫
            tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i (i₁ + i₃) ⋯) ≫
        ιTensorObj Y (tensorObj Z X) i₂ (i₁ + i₃) k ⋯
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂)) (β_ (X i₁) (Z i₃)).hom ≫
        MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂)) (ιTensorObj Z X i₃ i₁ (i₁ + i₃) ⋯) ≫
          ιTensorObj Y (tensorObj Z X) i₂ (i₁ + i₃) k ⋯

Tactic:
← MonoidalCategory.id_tensor_comp_assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂)) ((β_ (X i₁) (Z i₃)).hom ≫ ιTensorObj Z X i₃ i₁ (i₁ + i₃) ⋯) ≫
        ιTensorObj Y (tensorObj Z X) i₂ (i₁ + i₃) k ⋯
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 c ∈ (comap φ S).arrows c c

Tactic:
rw [comap, mem_ofPred, Functor.map_id]; apply Sn.wide

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ HasBiproduct F

Tactic:
by
          apply hasBiproduct_of_total (Biproducts.bicone F)
          simpa using! biproduct.map_eq.symm

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ {f | c = d ∧ f ∈ S.arrows c d} → Groupoid.inv p ∈ {f | d = c ∧ f ∈ S.arrows d c}

Tactic:
rintro _ _ _ ⟨rfl, h⟩; exact ⟨rfl, S.inv h⟩

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ∈ (full univ).arrows x✝² x✝¹ ↔ x✝ ∈ ⊤.arrows x✝² x✝¹

Tactic:
simp only [mem_full_iff, mem_univ, and_self, mem_top]

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 : B ⥤ C
G H : C ⥤ D
η : G ⟶ H
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F G).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F H).inv)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
G H : C ⥤ D
η : G ⟶ H
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F G).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft (mapWhiskerLeft (𝟭 A) η) ≫ (mapCompRight A F H).inv)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
η : F ⟶ G
H : C ⥤ D
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F H).hom ≫
            Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A G H).inv)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
η : F ⟶ G
H : C ⥤ D
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (Functor.whiskerRight η H))).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F H).hom ≫
            Functor.whiskerRight (mapWhiskerLeft (𝟭 A) η) (mapPair (𝟭 A) H) ≫ (mapCompRight A G H).inv)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
G : C ⥤ D
H : D ⥤ E
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
              ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
                (mapPair (𝟭 A) F).whiskerLeft (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
G : C ⥤ D
H : D ⥤ E
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) (F.associator G H).hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A (F ⋙ G) H).hom ≫
            Functor.whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
              ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
                (mapPair (𝟭 A) F).whiskerLeft (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A (𝟭 B) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A (𝟭 B) F).hom ≫
            Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
x✝ : A
⊢ ((inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclLeft A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝

Tactic:
simp [mapCompRight]

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 : B ⥤ C
x✝ : B
⊢ ((inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom)).app x✝ =
    ((inclRight A B).whiskerLeft
          ((mapCompRight A F (𝟭 C)).hom ≫
            (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)).app
      x✝

Tactic:
simp [mapCompRight]

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

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

Tactic:
intros; exact congr($(mapWhiskerRight_whiskerLeft D _ _).toCatHom₂)

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

Goal state before:
pp: I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫ fun i ↦ (c i).ι.app j') = (fun i ↦ (c i).ι.app j) ≫ ((Functor.const J).obj fun i ↦ (c i).pt).map f

Tactic:
funext i
        exact (c i).ι.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case inr
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)

Tactic:
have hc' := WithTerminal.isLimitEquiv.symm hc

Goal state after:
case inr
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 0 b.inl b.inr

Tactic:
by
  convert! IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
    <;> subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
⊢ IsClosedUnderColimitsOfShape (fun f ↦ Coequifibered f.hom) J

Tactic:
have : IsClosedUnderIsomorphisms fun f : Under F ↦ f.hom.Coequifibered :=
    ⟨fun {X Y} e ↦ by rw [← Under.w e.hom, Coequifibered.cancel_right_of_respectsIso]; simp⟩

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
⊢ IsClosedUnderColimitsOfShape (fun f ↦ Coequifibered f.hom) J
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
⊢ r = s

Tactic:
by
    by_contra r_ne_s
    have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
      rw [Cardinal.two_le_iff]
      exact ⟨_, _, r_ne_s⟩
    let md := Σ Z W : C, Z ⟶ W
    let α := #md
    apply not_le_of_gt (Cardinal.cantor α)
    let yp : C := ∏ᶜ fun _ : md => Y
    apply _root_.trans _ _
    · exact #(X ⟶ yp)
    · apply le_trans (Cardinal.power_le_power_right z)
      rw [Cardinal.power_def]
      apply le_of_eq
      rw [Cardinal.eq]
      refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
      · intro f
        ext k
        simp [yp]
      · intro f
        ext ⟨j⟩
        simp [yp]
    · apply Cardinal.mk_le_of_injective _
      · intro f
        exact ⟨_, _, f⟩
      · rintro f g k
        cases k
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: case e'_2
C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
inst✝ : Small.{w, u'} J
x✝ : Cᵒᵖ ⥤ Type w
hF : HasLimit F
X✝ Y✝ : Cᵒᵖ ⥤ Type w
f✝ : X✝ ⟶ Y✝
⊢ MorphismProperty.ofHoms (preservesLimitHomFamily F) f✝ ↔
    MorphismProperty.single
      (coconePtToShrinkYoneda (limit.cone F) (colimit.isColimit (F.leftOp ⋙ shrinkYoneda.{w, v, u}))) f✝

Tactic:
exact ⟨fun ⟨_⟩ ↦ ⟨⟨⟩⟩, fun ⟨_⟩ ↦ ⟨⟨hF⟩⟩⟩

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_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)

Tactic:
C₂

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_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)