mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.CategoryTheory.Elementwise

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
x✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : f = g
x : CC X
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
rw [h]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
⊢ reverse (reverse f) = f

Tactic:
by apply h.inv'

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : p.length + 1 = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
Nat.add_right_cancel_iff

Goal state after:
case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : p.length = n✝ + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

Tactic:
simp only [reverse_reverse]

Goal state after:
case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    φ.map val✝
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X : C
⊢ F.obj X = G.obj X

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ F.map f ≍ G.map f

Tactic:
rw [h]

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

Goal state before:
pp: case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I✝ : Type u₁
G F : Discrete I✝ ⥤ C
h : ∀ (i : I✝), G.obj { as := i } = F.obj { as := i }
I : Discrete I✝
⊢ G.obj I = F.obj I

Tactic:
rw [h]

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

Goal state before:
pp: J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)

Tactic:
rw [h]

Goal state after:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.left φ₁ = Hom.left φ₂

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.left = Y.left

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.right = Y.right

Tactic:
rw [h]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
X Y : C
f : X ⟶ Y
⊢ W f = W' f

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
⊢ mk f = mk f'

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ f ≫ f' ≫ h' = (f ≫ h) ≫ i'

Tactic:
hsq₂.w,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ f ≫ h ≫ i' = (f ≫ h) ≫ i'
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.map (𝟭 C) = P

Tactic:
by
  rw [map_id_eq_isoClosure, P.isoClosure_eq_self]

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x x' : X
h : x = x'
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x'

Tactic:
rw [h]

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by
  simp [← ofHom_epi_iff_surjective]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g

Tactic:
by
  rw [Equiv.symm_apply_eq]
  simp only [homEquiv_naturality_right, Equiv.apply_symm_apply]

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m = P.liftConeMorphism s ≫ i.hom

Tactic:
by
    rw [← i.comp_inv_eq]; apply P.uniq_cone_morphism

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = G.map (lift s)

Tactic:
rw [h]

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = ht.lift (G.mapCone s)
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ x ≤ y

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

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
⊢ (fromSkeleton C).Faithful

Tactic:
apply InducedCategory.faithful

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit.{w + 1})

Tactic:
rintro ⟨⟨p⟩, h⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1})
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
have : HasColimit ((D ⋙ E) ⋙ F) := h

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
this : HasColimit ((D ⋙ E) ⋙ F)
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type w
f : β → C
inst✝ : HasProduct f
P : C
p : (b : β) → P ⟶ f b
b : β
⊢ lift p ≫ π f b = p b

Tactic:
by
  simp only [limit.lift_π, Fan.mk_π_app]

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

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m = s.proj default ≫ e.inv

Tactic:
· simpa [← cancel_mono e.hom] using hm default

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
u : WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := u } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := u }

Tactic:
cases u

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := left } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := right } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
u : WalkingPair
⊢ (colimit.cocone (pair X Y)).ι.app { as := u } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    (BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := u }

Tactic:
cases u

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ (colimit.cocone (pair X Y)).ι.app { as := left } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    (BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ (colimit.cocone (pair X Y)).ι.app { as := right } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    (BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := right }
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X Y : StructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ Hom.right f = Hom.right g

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' Y'' : C
T T' : C ⥤ D
X Y : StructuredArrow S T
h : X = Y
⊢ X.right = Y.right

Tactic:
rw [h]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ m = I.lift (BinaryFan.swap t)

Tactic:
rw [h]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
⊢ m = I.lift (BinaryFan.swap t)

Tactic:
have h := I.uniq (BinaryFan.swap t) m
    rw [h]
    rintro ⟨j⟩
    specialize w ⟨WalkingPair.swap j⟩
    cases j <;> exact w

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m = R.lift (BinaryFan.assocInv P t)

Tactic:
rw [h]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
h : f = g
⊢ f.left = g.left

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ ∀ (X : StructuredArrow L R),
    (map₂ α β).map
          (((map₂IdIso L (𝟙 L) (R.rightUnitor.hom ≫ R.leftUnitor.inv) ⋯ ⋯).symm ≪≫
                  map₂Congr (𝟙 L) (R.rightUnitor.hom ≫ R.leftUnitor.inv) F.unitIso G.unitIso (α' ≫ G.inverse.map α)
                      ((R.associator G.functor G.inverse).inv ≫
                        Functor.whiskerRight β G.inverse ≫
                          (F.functor.associator R' G.inverse).hom ≫
                            F.functor.whiskerLeft β' ≫ (F.functor.associator F.inverse R).inv)
                      ?m.563 ?m.564 ≪≫
                    (map₂CompMap₂Iso α' β' α β).symm).hom.app
            X) ≫
        (map₂CompMap₂Iso α β α' β' ≪≫
                map₂Congr (α ≫ G.functor.map α')
                    ((R'.associator G.inverse G.functor).inv ≫
                      Functor.whiskerRight β' G.functor ≫
                        (F.inverse.associator R G.functor).hom ≫
                          F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv)
                    F.counitIso G.counitIso (𝟙 L') (R'.rightUnitor.hom ≫ R'.leftUnitor.inv) ?m.659 ?m.660 ≪≫
                  map₂IdIso L' (𝟙 L') (R'.rightUnitor.hom ≫ R'.leftUnitor.inv) ⋯ ⋯).hom.app
          ((map₂ α β).obj X) =
      𝟙 ((map₂ α β).obj X)

Tactic:
simp [map₂Congr]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
h : f = g
⊢ f.right = g.right

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f✝ g✝ : Under X✝
φ : f✝ ⟶ g✝
X Y : T
f g : X ⟶ Y
h : f = g
A : Under Y
⊢ (map f).obj A = (map g).obj A

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X Y : CostructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ f.left = g.left

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' Y'' : C
S S' : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ X.left = Y.left

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Under (F.obj X)
B' : T
e : F.obj B' ≅ B.right
f : X ⟶ B'
hf : F.map f = B.hom ≫ e.inv
⊢ (post F).essImage B

Tactic:
exact ⟨Under.mk f, ⟨Under.isoMk e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ data.mapZ (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) = 𝟙 (data.factorizationData (f.hom.app j)).Z

Tactic:
rw [← data.mapZ_id]

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ data.mapZ (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) = data.mapZ (𝟙 (Arrow.mk (f.hom.app j)))
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
⊢ ∀ (X : CostructuredArrow S T),
    (map₂ α β).map
          (((map₂IdIso (S.leftUnitor.hom ≫ S.rightUnitor.inv) T (𝟙 ((𝟭 D).obj T)) ⋯ ⋯).symm ≪≫
                  map₂Congr (S.leftUnitor.hom ≫ S.rightUnitor.inv) (𝟙 ((𝟭 D).obj T)) F.unitIso G.unitIso
                      ((F.functor.associator F.inverse S).hom ≫
                        F.functor.whiskerLeft α' ≫
                          (F.functor.associator U G.inverse).inv ≫
                            Functor.whiskerRight α G.inverse ≫ (S.associator G.functor G.inverse).hom)
                      (G.inverse.map β ≫ β') ?m.565 ?m.566 ≪≫
                    (map₂CompMap₂Iso α' β' α β).symm).hom.app
            X) ≫
        (map₂CompMap₂Iso α β α' β' ≪≫
                map₂Congr
                    ((F.inverse.associator F.functor U).hom ≫
                      F.inverse.whiskerLeft α ≫
                        (F.inverse.associator S G.functor).inv ≫
                          Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom)
                    (G.functor.map β' ≫ β) F.counitIso G.counitIso (U.leftUnitor.hom ≫ U.rightUnitor.inv)
                    (𝟙 ((𝟭 B).obj V)) ?m.661 ?m.662 ≪≫
                  map₂IdIso (U.leftUnitor.hom ≫ U.rightUnitor.inv) V (𝟙 ((𝟭 B).obj V)) ⋯ ⋯).hom.app
          ((map₂ α β).obj X) =
      𝟙 ((map₂ α β).obj X)

Tactic:
simp [map₂Congr]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f

Tactic:
rw [h]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f'
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case mk.mk.e_4
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ comp_zero✝¹ ≍ comp_zero✝

Tactic:
apply proof_irrel_heq

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

Goal state before:
pp: case mk.mk.e_5
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ zero_comp✝¹ ≍ zero_comp✝

Tactic:
apply proof_irrel_heq

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((Cone.functoriality F G).map ((limit.isLimit F).liftConeMorphism c))
⊢ IsIso ((limit.isLimit F).liftConeMorphism c)

Tactic:
by
        apply isIso_of_reflects_iso _ (Cone.functoriality F G)

Goal state after: