mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_2
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 Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
intro X Y f
      have (j : _) := Functor.congr_hom congr($((w j).symm).toFunctor) f
      simp [this, -homDiagram_obj, limit_π_homDiagram_eqToHom]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
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
⊢ W₁.Q.prod W₂.Q ⋙ prodLift F hF = F

Tactic:
rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C'
f g : x ⟶ y
⊢ (Sum.inr_ C C').map f = (Sum.inr_ C C').map g

Tactic:
((by assumption : IsDiscrete C').subsingleton x y).allEq f g

Goal state after:
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C'
f g : x ⟶ y
⊢ (Sum.inr_ C C').map g = (Sum.inr_ C C').map g
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
Q X Y Z : LocalizedMonoidal L W ε
f : X ⟶ Y
g : Y ⟶ Z
⊢ Q ◁ (f ≫ g) = Q ◁ f ≫ Q ◁ g

Tactic:
by
  simp only [← id_tensorHom, ← tensor_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
⊢ f = g

Tactic:
ext y
    · exact congr($h₁ y)
    · exact congr($h₂ y)

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

Goal state before:
pp: C : Type u_1
C' : Type ?u.4
D : Type u_2
D' : Type ?u.8
H : Type u_3
H' : Type ?u.12
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, ?u.4} C'
inst✝⁵ : Category.{v_3, u_2} D
inst✝⁴ : Category.{v_4, ?u.8} D'
inst✝³ : Category.{v_5, u_3} H
inst✝² : Category.{v_6, ?u.12} H'
LF'' LF' LF : D ⥤ H
F F' F'' : C ⥤ H
e : F ≅ F'
L : C ⥤ D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
α'₂ : L ⋙ LF' ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasLeftDerivedFunctor W
⊢ (F.totalLeftDerived L W).IsRightKanExtension (F.totalLeftDerivedCounit L W)

Tactic:
by
    dsimp [totalLeftDerived, totalLeftDerivedCounit]
    infer_instance

Goal state after:
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₁))
⊢ α.app X₁ ≫ 𝟙 (L₂.obj (G.obj X₁)) = α.app X₁

Tactic:
Category.comp_id

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₁))
⊢ α.app X₁ = α.app X₁
Module: Mathlib.CategoryTheory.Limits.FintypeCat

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).obj
i : ι
⊢ (ConcreteCategory.hom (Pi.π X i)) ((productEquiv X).symm x) = x i

Tactic:
← productEquiv_apply,

Goal state after:
ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).obj
i : ι
⊢ (productEquiv X) ((productEquiv X).symm x) i = x i
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ⋯
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)

Tactic:
have (X : I) : IsConnected X.val := hc X.val X.property

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this : ∀ (X : ↑I), IsConnected ↑X
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: G : Type u₁
inst✝ : Groupoid G
⊢ 𝟭 G ⋙ of G = of G

Tactic:
Functor.id_comp

Goal state after:
G : Type u₁
inst✝ : Groupoid G
⊢ of G = of G
Module: Mathlib.CategoryTheory.Groupoid.VertexGroup

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ δ ≫ 𝟙 d = δ

Tactic:
Category.comp_id

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ d : C
⊢ 𝟙 c✝ ≫ 𝟙 c✝ ∈ {p | Discrete.Arrows c✝ c✝ p}

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ d : C
⊢ 𝟙 c✝ ∈ {p | Discrete.Arrows c✝ c✝ p}
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = e.functor ⋙ 𝟭 D ⋙ e.inverse

Tactic:
Functor.id_comp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = e.functor ⋙ e.inverse
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ f.inverse ⋙ 𝟭 D ⋙ f.functor = 𝟭 E

Tactic:
Functor.id_comp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ f.inverse ⋙ f.functor = 𝟭 E
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl.refl.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
suffices Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map <| Groupoid.inv f ≫ γ ≫ f) by
        simp only [inv_eq_inv, Functor.map_comp, Functor.map_inv] at this; exact this

Goal state after:
case refl.refl.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
i : s.pt.I
a : α
w✝ : ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).f = (s.proj a).f
hm :
  ∀ (i : s.pt.I), ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).φ i ≫ eqToHom ⋯ = (s.proj a).φ i
⊢ (φ i ≫ 𝟙 (∏ᶜ U.obj ∘ fun a ↦ (s.proj a).f i)) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a =
    (Pi.lift fun a ↦ (s.proj a).φ i) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a

Tactic:
simpa using hm i

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ whiskerRight (edgeTransform C D) G ≫ (Prod.snd C D).whiskerLeft eᵣ.inv =
    (Prod.fst C D).whiskerLeft eₗ.inv ≫ whiskerRight (edgeTransform C D) F

Tactic:
Eq.comm,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ (Prod.fst C D).whiskerLeft eₗ.inv ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ (Prod.snd C D).whiskerLeft eᵣ.inv
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ whiskerRight (edgeTransform C D) F =
    (((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G) ≫
      ((Prod.snd C D).isoWhiskerLeft eᵣ).inv

Tactic:
Eq.comm,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ (((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G) ≫
      ((Prod.snd C D).isoWhiskerLeft eᵣ).inv =
    whiskerRight (edgeTransform C D) F
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: 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ᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ shrinkYoneda.{w, v, u}.map (F.map f.unop).unop ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    (shrinkYoneda.{w, v, u}.map (F.map f.unop).unop ≫ shrinkYonedaEquiv.symm (↑s (unop j₂))) ≫ 𝟙 P

Tactic:
Category.comp_id

Goal state after:
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ᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ shrinkYoneda.{w, v, u}.map (F.map f.unop).unop ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYoneda.{w, v, u}.map (F.map f.unop).unop ≫ shrinkYonedaEquiv.symm (↑s (unop j₂))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
left✝¹ : IsIso f.left
left✝ : IsIso f.base
right✝ : IsIso f.right
⊢ IsIso f

Tactic:
use mkIso (asIso f.left) (asIso f.right) (asIso f.base)
      f.left_coherence f.right_coherence |>.inv

Goal state after:
case h
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
left✝¹ : IsIso f.left
left✝ : IsIso f.base
right✝ : IsIso f.right
⊢ f ≫ (mkIso (asIso f.left) (asIso f.right) (asIso f.base) ⋯ ⋯).inv = 𝟙 ψ' ∧
    (mkIso (asIso f.left) (asIso f.right) (asIso f.base) ⋯ ⋯).inv ≫ f = 𝟙 ψ'
Module: Mathlib.CategoryTheory.Localization.FiniteProducts

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
J : Type
inst✝³ : HasProductsOfShape J C
inst✝² : W.IsStableUnderProductsOfShape J
inst✝¹ : W.ContainsIdentities
inst✝ : Finite J
⊢ (whiskeringRight (Discrete J) C D).obj L ⋙ limitFunctor L W J ≅ lim ⋙ L

Tactic:
by
  apply Localization.fac

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
⊢ G.map f.snd = x.iso.inv ≫ F.map f.fst ≫ y.iso.hom

Tactic:
Eq.comm,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
⊢ x.iso.inv ≫ F.map f.fst ≫ y.iso.hom = G.map f.snd
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case comp_id
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✝ : 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)
⊢ projectMapAux f✝¹ f✝ ≫ 𝟙 (projectObj f✝¹ Y✝) = projectMapAux f✝¹ f✝

Tactic:
Category.comp_id

Goal state after:
case comp_id
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✝ : 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)
⊢ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f✝
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ 𝟙 (L.obj X₁ ⊗ L.obj X₂))

Tactic:
Category.comp_id

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
⊢ f ⊙ₗₘ g ⊙ₗₘ h = (αₗ c₁ c₃ d₁).inv ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ (αₗ c₂ c₄ d₂).hom

Tactic:
Eq.comm,

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
⊢ (αₗ c₁ c₃ d₁).inv ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ (αₗ c₂ c₄ d₂).hom = f ⊙ₗₘ g ⊙ₗₘ h
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
d d' : D
f : d ⟶ d'
⊢ 𝟙_ C ⊴ₗ f = ((λₗ d).hom ≫ f) ≫ (λₗ d').inv

Tactic:
Eq.comm,

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
d d' : D
f : d ⟶ d'
⊢ ((λₗ d).hom ≫ f) ≫ (λₗ d').inv = 𝟙_ C ⊴ₗ f
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ (f ⊙ᵣₘ g) ⊙ᵣₘ h = (αᵣ d₁ c₁ c₃).inv ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ (αᵣ d₂ c₂ c₄).hom

Tactic:
Eq.comm,

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ (αᵣ d₁ c₁ c₃).inv ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ (αᵣ d₂ c₂ c₄).hom = (f ⊙ᵣₘ g) ⊙ᵣₘ h
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d d' : D
f : d ⟶ d'
⊢ f ⊵ᵣ 𝟙_ C = ((ρᵣ d).hom ≫ f) ≫ (ρᵣ d').inv

Tactic:
Eq.comm,

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d d' : D
f : d ⟶ d'
⊢ ((ρᵣ d).hom ≫ f) ≫ (ρᵣ d').inv = f ⊵ᵣ 𝟙_ C
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ 𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
by
  refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
  apply (initialIsInitial.ofIso (mulZero initialIsInitial).symm).hom_ext

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X = 𝟙_ C ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X

Tactic:
comp_actionHomLeft,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X = 𝟙_ C ⊴ₗ e₂.inv ≫ η ⊵ₗ X ≫ e₁.inv ⊵ₗ X