mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Tactic:
mem_nhds_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
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ∃ t ⊆ ⇑(toAut F G) ⁻¹' A, IsOpen t ∧ 1 ∈ t
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
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
t : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).obj
φ : Aut X
hg :
  g • (ConcreteCategory.hom (F.map φ.hom)) y = (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map φ.hom)) y)
this : Function.Injective ⇑(ConcreteCategory.hom (F.map φ.hom))
⊢ (ConcreteCategory.hom (F.map φ.hom)) (g • y) =
    (ConcreteCategory.hom (F.map φ.hom)) ((ConcreteCategory.hom (t.app X)) y)

Tactic:
IsNaturalSMul.naturality,

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
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
t : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).obj
φ : Aut X
hg :
  g • (ConcreteCategory.hom (F.map φ.hom)) y = (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map φ.hom)) y)
this : Function.Injective ⇑(ConcreteCategory.hom (F.map φ.hom))
⊢ g • (ConcreteCategory.hom (F.map φ.hom)) y = (ConcreteCategory.hom (F.map φ.hom)) ((ConcreteCategory.hom (t.app X)) y)
Module: Mathlib.CategoryTheory.Join.Sum

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
x y : C ⊕ D
h h' : x ⟶ y
heq : (fromSum C D).map h = (fromSum C D).map h'
⊢ h = h'

Tactic:
cases h <;> cases h'

Goal state after:
case inl.inl
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : C
f✝¹ f✝ : x✝ ⟶ y✝
heq : (fromSum C D).map ((Sum.inl_ C D).map f✝¹) = (fromSum C D).map ((Sum.inl_ C D).map f✝)
⊢ (Sum.inl_ C D).map f✝¹ = (Sum.inl_ C D).map f✝

case inr.inr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : D
f✝¹ f✝ : x✝ ⟶ y✝
heq : (fromSum C D).map ((Sum.inr_ C D).map f✝¹) = (fromSum C D).map ((Sum.inr_ C D).map f✝)
⊢ (Sum.inr_ C D).map f✝¹ = (Sum.inr_ C D).map f✝
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj zero ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := zero, right := { as := as✝ }, hom := φ } (mk ⋯.some)

Tactic:
apply h₂

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

Goal state before:
pp: 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
⊢ mapWhiskerRight (F.whiskerLeft η) (𝟭 D) =
    (mapCompLeft D F G).hom ≫ (mapPair F (𝟭 D)).whiskerLeft (mapWhiskerRight η (𝟭 D)) ≫ (mapCompLeft D F H).inv

Tactic:
apply natTrans_ext <;> ext <;> simp [mapCompLeft]

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

Goal state before:
pp: 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
⊢ mapWhiskerRight (Functor.whiskerRight η H) (𝟭 D) =
    (mapCompLeft D F H).hom ≫ Functor.whiskerRight (mapWhiskerRight η (𝟭 D)) (mapPair H (𝟭 D)) ≫ (mapCompLeft D G H).inv

Tactic:
apply natTrans_ext <;> ext <;> simp [mapCompLeft]

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

Goal state before:
pp: 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
⊢ mapWhiskerRight (F.associator G H).hom (𝟭 E) =
    (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

Tactic:
apply natTrans_ext <;> ext <;> simp [mapCompLeft]

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

Goal state before:
pp: 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
⊢ mapWhiskerRight F.leftUnitor.hom (𝟭 C) =
    (mapCompLeft C (𝟭 A) F).hom ≫
      Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom

Tactic:
apply natTrans_ext <;> ext <;> simp [mapCompLeft]

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

Goal state before:
pp: 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
⊢ mapWhiskerRight F.rightUnitor.hom (𝟭 C) =
    (mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom

Tactic:
apply natTrans_ext <;> ext <;> simp [mapCompLeft]

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

Goal state before:
pp: case edge
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 F' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
c : C
d : D
⊢ (F.map (edge c d) ≫
      match right d with
      | left x => αₗ.app x
      | right x => αᵣ.app x) =
    (match left c with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map (edge c d)

Tactic:
exact funext_iff.mp (NatTrans.ext_iff.mp h) (c, d)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
⊢ Nonempty (h.LiftStruct g₁ g₂ b)

Tactic:
obtain ⟨l, h₁, h₂⟩ := h.isPullback.exists_lift g₁ g₂ w
  exact ⟨{
    f := l
    f_p₁ := h₁
    f_p₂ := h₂
    f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁] }⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
⊢ (((Functor.const ℕᵒᵖ).obj (∏ᶜ M)).map (homOfLE ⋯).op ≫
        Pi.map fun m ↦ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    ((Pi.map fun m ↦ if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m

Tactic:
simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, homOfLE_leOfHom,
      Functor.const_obj_map, Category.id_comp, Pi.map_π, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, Category.assoc, Pi.map_π_assoc]

Goal state after:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
⊢ (Pi.π M m ≫ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯) =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
⊢ (Pi.π M m ≫ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯) =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯

Tactic:
split

Goal state after:
case isTrue
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h✝ : m < n
⊢ Pi.π M m ≫ eqToHom ⋯ = Pi.π M m ≫ (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫ eqToHom ⋯

case isFalse
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h✝ : ¬m < n
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case isFalse
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h✝ : ¬m < n
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯

Tactic:
split

Goal state after:
case isFalse.isTrue
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h✝¹ : ¬m < n
h✝ : m < n + 1
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ = Pi.π M m ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ f m ≫ eqToHom ⋯

case isFalse.isFalse
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h✝¹ : ¬m < n
h✝ : ¬m < n + 1
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ = Pi.π M m ≫ (f m ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ (∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x') → coendRel F ⟨j, x⟩ ⟨j', x'⟩

Tactic:
· rintro ⟨f, y, rfl, rfl⟩
    exact coendRel.mk f y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
⊢ Epi
    (if h : ↑⟨val✝, property✝⟩ < n then eqToHom ⋯
    else if h' : ↑⟨val✝, property✝⟩ < n + 1 then eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
split

Goal state after:
case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯)

case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
⊢ IsIso
    (if h : ↑⟨val✝, property✝⟩ < n then eqToHom ⋯
    else if h' : ↑⟨val✝, property✝⟩ < n + 1 then eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
split

Goal state after:
case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)

case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)
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₆
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'
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 : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.left ≫ e.inv.left = 𝟙 ψ.left

Tactic:
by simp [← category_comp_left]

Goal state after:
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₆
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'
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 : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.left ≫ e.hom.left = 𝟙 ψ'.left

Tactic:
by simp [← category_comp_left]

Goal state after:
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₆
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'
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 : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.right ≫ e.inv.right = 𝟙 ψ.right

Tactic:
by simp [← category_comp_right]

Goal state after:
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₆
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'
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 : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.right ≫ e.hom.right = 𝟙 ψ'.right

Tactic:
by simp [← category_comp_right]

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

Goal state before:
pp: case h_option.refine_1.some
J : Type w
inst✝⁴ : Fintype 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 : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
hf₁ : W none f.1
hf₂ : MorphismProperty.pi (fun j ↦ W (some j)) f.2
i : J
⊢ W (some i) ((Pi.optionEquivalence C).inverse.map f (some i))

Tactic:
apply hf₂

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

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    rintro X Y ⟨f⟩
    exact Quotient.sound (id_comp f)

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ (pullbackPushforwardAdj (𝟙 I)).unit ≫
      (pullback (𝟙 I)).whiskerLeft
        ((pullbackPushforwardAdj (𝟙 I)).rightAdjointUniq (pullbackPushforwardAdj (𝟙 I))).hom =
    (pullbackPushforwardAdj (𝟙 I)).unit

Tactic:
Adjunction.unit_rightAdjointUniq_hom

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ (pullbackPushforwardAdj (𝟙 I)).unit = (pullbackPushforwardAdj (𝟙 I)).unit
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ (pullbackPushforwardAdj (f ≫ g)).unit ≫
      (pullback (f ≫ g)).whiskerLeft
        ((pullbackPushforwardAdj (f ≫ g)).rightAdjointUniq (pullbackPushforwardAdj (f ≫ g))).hom =
    (pullbackPushforwardAdj (f ≫ g)).unit

Tactic:
Adjunction.unit_rightAdjointUniq_hom

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ (pullbackPushforwardAdj (f ≫ g)).unit = (pullbackPushforwardAdj (f ≫ g)).unit
Module: Mathlib.CategoryTheory.Monoidal.Multifunctor

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalCategory D
F₁ F₂ : C ⥤ D
f : F₁ ⟶ F₂
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : C
⊢ ((curriedTensorPre F₁).map x✝¹ ≫ { app := fun X₂ ↦ f.app x✝² ⊗ₘ f.app X₂, naturality := ⋯ }).app x✝ =
    ({ app := fun X₂ ↦ f.app x✝³ ⊗ₘ f.app X₂, naturality := ⋯ } ≫ (curriedTensorPre F₂).map x✝¹).app x✝

Tactic:
simp [← tensorHom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ T.η.app X.of ≫ T.map f.of ≫ T.μ.app Y.of = f.of

Tactic:
← T.η.naturality_assoc f.of,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ (𝟭 C).map f.of ≫ T.η.app (T.obj Y.of) ≫ T.μ.app Y.of = f.of
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 = (αₗ c₁ c₃ d₁).inv ≫ ((f ⊗ₘ g) ⊙ₗₘ h)

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]

Goal state after:
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 = (αᵣ d₁ c₁ c₃).inv ≫ (f ⊙ᵣₘ g ⊗ₘ h)

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
x : X ⟶ H
z : X ⟶ G
⊢ (monoidHom φ X) (lift z x ≫ ψ) = z * (monoidHom φ X) x * z⁻¹

Tactic:
by simp [hψ]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
X Y : D
⊢ IsIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))

Tactic:
apply Functor.essImage.unit_isIso
            have := reflective_products i
            use Limits.prod X Y
            constructor
            apply Limits.PreservesLimitPair.iso i _ _ |>.trans
            refine Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
              (tensorProductIsBinaryProduct _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case e
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
X Y : D
⊢ ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))).pt ≅
    (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).pt

Tactic:
change (reflector i ⋙ i).obj (i.obj X ⊗ i.obj Y) ≅ (𝟭 C).obj (i.obj X ⊗ i.obj Y)
          letI : IsIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) := by
            apply Functor.essImage.unit_isIso
            have := reflective_products i
            use Limits.prod X Y
            constructor
            apply Limits.PreservesLimitPair.iso i _ _ |>.trans
            refine Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
              (tensorProductIsBinaryProduct _ _)
          exact asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) |>.symm

Goal state after: