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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ α.hom ≫ f = 𝟙 X ↔ f = α.inv

Tactic:
rw [← eq_inv_comp, comp_id]

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

Goal state before:
pp: case mp.inl
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝)

pp: case mp.inr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case mp.inl
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝)

case mp.inr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝)
Module: Mathlib.CategoryTheory.NatIso

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
X✝ Y✝ : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
⊢ G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f

Tactic:
have h := congr_arg (fun f => (app X).inv ≫ f ≫ (app Y).inv) (naturality f).symm
        simp only [Iso.inv_hom_id_assoc, Iso.hom_inv_id, assoc, comp_id] at h
        exact h

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F G : C ⥤ D
φ : F ⟶ G
X Y : C
f : X ⟶ Y
x : ToType (F.obj X)
⊢ (ConcreteCategory.hom (φ.app Y)) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (φ.app X)) x)

Tactic:
by
  simp [← CategoryTheory.comp_apply]

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ = a h✝¹

pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : ¬q
⊢ a h✝¹ = a h✝¹

pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ h✝ = c h✝¹ ⋯

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ = a h✝¹

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : ¬q
⊢ a h✝¹ = a h✝¹

case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ h✝ = c h✝¹ ⋯
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ h✝ = a h✝¹ ⋯

pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : ¬q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : q
⊢ c h✝¹ = c h✝¹

pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ = c h✝¹

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ h✝ = a h✝¹ ⋯

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : ¬q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : q
⊢ c h✝¹ = c h✝¹

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ = c h✝¹
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f p

pp: case neg
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f p

Tactic:
<;>

Goal state after:
case pos
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f p

case neg
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f p
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f True

pp: case neg
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f False

Tactic:
<;>

Goal state after:
case pos
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f True

case neg
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f False
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ p → f True

pp: case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ ¬p → f False

Tactic:
<;>

Goal state after:
case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ p → f True

case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ ¬p → f False
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ f True

pp: case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ f False

Tactic:
<;>

Goal state after:
case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ f True

case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ f False
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ True ↔ p

pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ False ↔ p

Tactic:
<;>

Goal state after:
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ True ↔ p

f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ False ↔ p
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case inl
f : Prop → Prop
h : f True
⊢ ∃ p, f p

pp: case inr
f : Prop → Prop
h : f False
⊢ ∃ p, f p

Tactic:
<;>

Goal state after:
case inl
f : Prop → Prop
h : f True
⊢ ∃ p, f p

case inr
f : Prop → Prop
h : f False
⊢ ∃ p, f p
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil

Tactic:
simp at hzero

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

Goal state before:
pp: case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : u✝ ⟶ v✝
⊢ φ.symmetrify.map (reverse (Sum.inl val✝)) = reverse (φ.symmetrify.map (Sum.inl val✝))

pp: case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : v✝ ⟶ u✝
⊢ φ.symmetrify.map (reverse (Sum.inr val✝)) = reverse (φ.symmetrify.map (Sum.inr val✝))

Tactic:
<;>

Goal state after:
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : u✝ ⟶ v✝
⊢ φ.symmetrify.map (reverse (Sum.inl val✝)) = reverse (φ.symmetrify.map (Sum.inl val✝))

case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : v✝ ⟶ u✝
⊢ φ.symmetrify.map (reverse (Sum.inr val✝)) = reverse (φ.symmetrify.map (Sum.inr val✝))
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToHom p ≫ eqToHom q = eqToHom ⋯

Tactic:
by
  cases p
  cases q
  simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ G.obj Y = F.obj Y

Tactic:
by rw [hY]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ F.obj Y = G.obj Y

Tactic:
by rw [hY]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
Z' : C
h : unop X ⟶ Z'
⊢ (f ≫ g).unop ≫ h = g.unop ≫ f.unop ≫ h

Tactic:
by
  simp only [unop_comp, Category.assoc]

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

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

Tactic:
ext
  exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ (⨅ i, W i).RespectsLeft Q

Tactic:
by
  rw [← sInf_range]
  exact sInf (by simpa)

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ (⨅ i, W i).RespectsRight Q

Tactic:
by
  rw [← sInf_range]
  exact sInf (by simpa)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsIso
⊢ (⨅ i, W i).RespectsIso

Tactic:
by
  rw [← sInf_range]
  exact sInf (by simpa)

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)

Tactic:
<;>

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)

pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)

Tactic:
<;>

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)

case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)

pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)

Tactic:
<;>

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)

case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
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
x✝¹ x✝ : ThinSkeleton C
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b

Tactic:
by
    rintro ⟨⟨f₁⟩⟩ ⟨⟨_⟩⟩
    rfl

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p → HasLiftingProperty i' p

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i' p → HasLiftingProperty i p

Tactic:
<;>

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p → HasLiftingProperty i' p

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i' p → HasLiftingProperty i p
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
F : C ⥤ D
⊢ F.map (𝟙 X) = 𝟙 (F.obj X)

Tactic:
F.map_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
F : C ⥤ D
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.left
      (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk f.op))

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.right
      (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk f.op))

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.left
      (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk f.op))

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.right
      (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk f.op))
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.left
      (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk f.unop))

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.right
      (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk f.unop))

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.left
      (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk f.unop))

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.Hom.right
      (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯ ≫
        Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk f.unop))
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.left (Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (τ.app X)))

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.right (Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (τ.app X)))

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.left (Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (τ.app X)))

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.right (Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (τ.app X)))
Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f → StrongEpi g

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi g → StrongEpi f

Tactic:
<;>

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f → StrongEpi g

case mpr
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi g → StrongEpi f
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p → HasLiftingProperty i (F.map p)

pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i (F.map p) → HasLiftingProperty (G.map i) p

Tactic:
<;>

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p → HasLiftingProperty i (F.map p)

case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i (F.map p) → HasLiftingProperty (G.map i) p
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ HasLiftingProperty i (F.map p)

pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ HasLiftingProperty (G.map i) p

Tactic:
<;>

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ HasLiftingProperty i (F.map p)

case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ HasLiftingProperty (G.map i) p
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift

pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), sq.HasLift

Tactic:
<;>

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift

case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), sq.HasLift