awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsSplitMono f
⊢ IsSplitEpi.{v₁, u₁} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op

Tactic:
.mk' IsSplitMono.exists_splitMono.some.op

Premises used: CategoryTheory.SplitMono.op, Nonempty.some, CategoryTheory.IsSplitMono.exists_splitMono, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X Y : C
p : X = Y
rw : Y ⟶ Y
⊢ X ⟶ Y

Tactic:
rw [p]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X Y : C
p : X = Y
⊢ Y ⟶ Y

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X : C
p : X = X
⊢ Eq.{v₁ + 1} (α := X ⟶ X) (eqToHom p) (𝟙 X)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
refl : ∀ (q : X = Z), Eq.{v₁ + 1} (α := X ⟶ Z) (eqToHom ⋯ ≫ eqToHom q) (eqToHom ⋯)
⊢ Eq.{v₁ + 1} (α := X ⟶ Z) (eqToHom p ≫ eqToHom q) (eqToHom ⋯)

Tactic:
cases p
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
q : X = Z
refl : Eq.{v₁ + 1} (α := X ⟶ X) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{v₁ + 1} (α := X ⟶ Z) (eqToHom ⋯ ≫ eqToHom q) (eqToHom ⋯)

Tactic:
cases q
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := X ⟶ X) (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : X = Y
subst : HEq.{v₁ + 1} (α := X ⟶ X) (eqToHom ⋯) (β := X ⟶ X) (𝟙 X)
⊢ HEq.{v₁ + 1} (α := X ⟶ Y) (eqToHom h) (β := X ⟶ X) (𝟙 X)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ HEq.{v₁ + 1} (α := X ⟶ X) (eqToHom ⋯) (β := X ⟶ X) (𝟙 X)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : X = Y
subst : HEq.{v₁ + 1} (α := X ⟶ X) (eqToHom ⋯) (β := X ⟶ X) (𝟙 X)
⊢ HEq.{v₁ + 1} (α := X ⟶ Y) (eqToHom h) (β := Y ⟶ Y) (𝟙 Y)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
h : W = Y
h' : X = Z
refl : ∀ (g : W ⟶ Z), f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g
⊢ f = eqToHom h ≫ g ≫ eqToHom ⋯ ↔ f ≍ g

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
refl : ∀ (g : W ⟶ X), f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g

Tactic:
cases h'
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X : C
f g : W ⟶ X
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
h : W = Y
h' : Z = X
⊢ f = eqToHom h ≫ g ≫ eqToHom h' ↔ f ≍ g

Tactic:
conj_eqToHom_iff_heq _ _ _ h'.symm

Premises used: CategoryTheory.conj_eqToHom_iff_heq, Eq.symm
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f ≫ eqToHom p = g
⊢ f = g ≫ eqToHom ⋯

Tactic:
simp [← h]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f = g ≫ eqToHom ⋯
⊢ f ≫ eqToHom p = g

Tactic:
simp [eq_whisker h (eqToHom p)]

Premises used: CategoryTheory.eq_whisker, CategoryTheory.eqToHom
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : eqToHom p ≫ g = f
⊢ g = eqToHom ⋯ ≫ f

Tactic:
simp [← h]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : g = eqToHom ⋯ ≫ f
⊢ eqToHom p ≫ g = f

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y : C
f : Y ⟶ X
h : W = Y
rw : eqToHom h ≫ f = eqToHom h ≫ f ≫ eqToHom ⋯
rw₁ : eqToHom h ≫ f = eqToHom h ≫ f ≫ 𝟙 X
rw₂ rw₃ : eqToHom h ≫ f = eqToHom h ≫ f
⊢ eqToHom h ≫ f ≍ f

Tactic:
rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.conj_eqToHom_iff_heq, rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z Z' : C
f : Y ⟶ X
g : Z ⟶ Z'
h : W = Y
⊢ eqToHom h ≫ f ≍ g ↔ f ≍ g

Tactic:
⟨(eqToHom_comp_heq ..).symm.trans, (eqToHom_comp_heq ..).trans⟩

Premises used: HEq.symm, HEq.trans, CategoryTheory.eqToHom_comp_heq, Iff.intro
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z Z' : C
f : Y ⟶ X
g : Z ⟶ Z'
h : W = Y
⊢ g ≍ eqToHom h ≫ f ↔ g ≍ f

Tactic:
⟨(·.trans (eqToHom_comp_heq ..)), (·.trans (eqToHom_comp_heq ..).symm)⟩

Premises used: HEq.symm, HEq.trans, CategoryTheory.eqToHom_comp_heq, Iff.intro
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
h : Y = Z
rw : f ≫ eqToHom h = eqToHom ⋯ ≫ f ≫ eqToHom h
rw₁ : f ≫ eqToHom h = 𝟙 X ≫ f ≫ eqToHom h
rw₂ rw₃ : f ≫ eqToHom h = f ≫ eqToHom h
⊢ f ≫ eqToHom h ≍ f

Tactic:
rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]

Premises used: CategoryTheory.conj_eqToHom_iff_heq', CategoryTheory.eqToHom_refl, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z Z' : C
f : X ⟶ Y
g : Z ⟶ Z'
h : Y = W
⊢ f ≫ eqToHom h ≍ g ↔ f ≍ g

Tactic:
⟨(comp_eqToHom_heq ..).symm.trans, (comp_eqToHom_heq ..).trans⟩

Premises used: HEq.symm, HEq.trans, Iff.intro, CategoryTheory.comp_eqToHom_heq
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z Z' : C
f : X ⟶ Y
g : Z ⟶ Z'
h : Y = W
⊢ g ≍ f ≫ eqToHom h ↔ g ≍ f

Tactic:
⟨(·.trans (comp_eqToHom_heq ..)), (·.trans (comp_eqToHom_heq ..).symm)⟩

Premises used: HEq.symm, HEq.trans, Iff.intro, CategoryTheory.comp_eqToHom_heq
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
eq1 : X = X'
eq2 : Y = Y'
eq3 : Z = Z'
H1 : f ≍ f'
H2 : g ≍ g'
⊢ f ≫ g ≍ f' ≫ g'

Tactic:
grind
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
refl : z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j'

Tactic:
cases w
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j : β
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
refl : (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).hom
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').hom

Tactic:
cases w
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
refl : (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).inv
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').inv

Tactic:
cases w
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
refl : ∀ (q : X ⟶ Z), cast ⋯ q = eqToHom ⋯ ≫ q
⊢ cast ⋯ q = eqToHom p ≫ q

Tactic:
cases p
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ cast ⋯ q = eqToHom ⋯ ≫ q

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
refl : ∀ (q : X ⟶ Z), Eq.mpr ⋯ q = eqToHom ⋯ ≫ q
⊢ Eq.mpr ⋯ q = eqToHom p ≫ q

Tactic:
cases p
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ Eq.mpr ⋯ q = eqToHom ⋯ ≫ q

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
refl : cast ⋯ p = p ≫ eqToHom ⋯
⊢ cast ⋯ p = p ≫ eqToHom ⋯

Tactic:
cases q
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ cast ⋯ p = p ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
refl : Eq.mpr ⋯ p = p ≫ eqToHom ⋯
⊢ Eq.mpr ⋯ p = p ≫ eqToHom ⋯

Tactic:
cases q
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ Eq.mpr ⋯ p = p ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
X Y : C
p : X = Y
⊢ Eq.{v₁ + 1} (α := X ⟶ X) (eqToHom p ≫ eqToHom ⋯) (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
X Y : C
p : X = Y
⊢ Eq.{v₁ + 1} (α := Y ⟶ Y) (eqToHom ⋯ ≫ eqToHom p) (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
p : X = Y
⊢ Eq.{v₁ + 1} (α := X ⟶ Y) (Iso.hom (eqToIso p)) (eqToHom p)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
p : X = Y
⊢ Eq.{v₁ + 1} (α := Y ⟶ X) (Iso.inv (eqToIso p)) (eqToHom ⋯)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
p : X = X
⊢ Eq.{v₁ + 1} (α := X ≅ X) (eqToIso p) (Iso.refl X)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
w : Eq.{v₁ + 1} (α := X ⟶ Z) (Iso.hom (eqToIso p ≪≫ eqToIso q)) (Iso.hom (eqToIso ⋯))
⊢ Eq.{v₁ + 1} (α := X ≅ Z) (eqToIso p ≪≫ eqToIso q) (eqToIso ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ Eq.{v₁ + 1} (α := X ⟶ Z) (Iso.hom (eqToIso p ≪≫ eqToIso q)) (Iso.hom (eqToIso ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : X = Y
refl : Eq.{v₁ + 1} (α := op X ⟶ op X) (Quiver.Hom.op (eqToHom ⋯)) (eqToHom ⋯)
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op X) (Quiver.Hom.op (eqToHom h)) (eqToHom ⋯)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := op X ⟶ op X) (Quiver.Hom.op (eqToHom ⋯)) (eqToHom ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
h : X = Y
refl : Eq.{v₁ + 1} (α := unop X ⟶ unop X) (Quiver.Hom.unop (eqToHom ⋯)) (eqToHom ⋯)
⊢ Eq.{v₁ + 1} (α := unop Y ⟶ unop X) (Quiver.Hom.unop (eqToHom h)) (eqToHom ⋯)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := unop X ⟶ unop X) (Quiver.Hom.unop (eqToHom ⋯)) (eqToHom ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
X Y : C
h : X = Y
⊢ IsIso.{v₁, u₁} (eqToHom h)

Tactic:
(eqToIso h).isIso_hom

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
F_obj : C → D
map : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
G_obj : C → D
map_1 : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (G_obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.obj X =
      { obj := G_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.map f =
      eqToHom ⋯ ≫
        { obj := G_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.map
            f ≫
          eqToHom ⋯
h : ∀ (X : C), F_obj X = G_obj X
⊢ F_obj = G_obj

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
F_obj : C → D
map : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
G_obj : C → D
map_1 : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (G_obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.obj X =
      { obj := G_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.map f =
      eqToHom ⋯ ≫
        { obj := G_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.map
            f ≫
          eqToHom ⋯
X : C
⊢ F_obj X = G_obj X

Tactic:
apply h_obj
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
F_obj : C → D
map : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
G_obj : C → D
map_1 : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (G_obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.obj X =
      { obj := G_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.map f =
      eqToHom ⋯ ≫
        { obj := G_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.map
            f ≫
          eqToHom ⋯
obtain :
  ∀ (map_2 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)) (map_id_2 : ∀ (X : C), map_2 (𝟙 X) = 𝟙 (F_obj X))
    (map_comp_2 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g)
    (h_obj :
      ∀ (X : C),
        { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.obj X =
          { obj := F_obj, map := @map_2, map_id := map_id_2, map_comp := @map_comp_2 :
                Functor.{v₁, v₂, u₁, u₂} C D }.obj
            X)
    (h_map :
      ∀ (X Y : C) (f : X ⟶ Y),
        { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.map f =
          eqToHom ⋯ ≫
            { obj := F_obj, map := @map_2, map_id := map_id_2, map_comp := @map_comp_2 :
                    Functor.{v₁, v₂, u₁, u₂} C D }.map
                f ≫
              eqToHom ⋯),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
      { obj := F_obj, map := @map_2, map_id := map_id_2, map_comp := @map_comp_2 }
⊢ { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := G_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
obtain rfl : F_obj = G_obj := by
      ext X
      apply h_obj

Premises used: rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
F_obj : C → D
map : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.obj X =
      { obj := F_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.map f =
      eqToHom ⋯ ≫
        { obj := F_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.map
            f ≫
          eqToHom ⋯
e_map : @map = @map_1
⊢ { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := F_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
F_obj : C → D
map : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.obj X =
      { obj := F_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.map f =
      eqToHom ⋯ ≫
        { obj := F_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.map
            f ≫
          eqToHom ⋯
e_map : ∀ (X Y : C) (f : X ⟶ Y), map f = map_1 f
⊢ @map = @map_1

Tactic:
funext X Y f
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
F_obj : C → D
map : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.obj X =
      { obj := F_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.map f =
      eqToHom ⋯ ≫
        { obj := F_obj, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₂, u₁, u₂} C D }.map
            f ≫
          eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ map f = map_1 f

Tactic:
simpa using h_map X Y f
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
⊢ F = G

Tactic:
match F, G with
  | mk F_obj _ _ _, mk G_obj _ _ _ =>
    obtain rfl : F_obj = G_obj := by
      ext X
      apply h_obj
    congr
    funext X Y f
    simpa using h_map X Y f
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
rw : F.map f ≫ e.hom.app Y = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₁ : e.hom.app X ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₂ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₃ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₄ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ (G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₅ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯ ≫ eqToHom ⋯
rw₆ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
rw₇ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ 𝟙 (G.obj Y)
rw₈ rw₉ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_refl, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.eqToHom_trans
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f ≍ G.map f
⊢ F = G

Tactic:
Functor.ext h_obj fun _ _ f => (conj_eqToHom_iff_heq _ _ (h_obj _) (h_obj _)).2 <| h_map _ _ f

Premises used: Iff.mpr, CategoryTheory.Functor.ext, CategoryTheory.Functor.map, CategoryTheory.conj_eqToHom_iff_heq
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F = G
X : C
rw rw₁ : G.obj X = G.obj X
⊢ F.obj X = G.obj X

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F = G
X Y : C
f : X ⟶ Y
subst : F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
subst h