awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (goal)
Goal:
V_1 : Type u'
inst : Category.{v', u'} V_1
inst_1 : MonoidalCategory.{v', u'} V_1
C_1 : Type u
inst_2 : Category.{v, u} C_1
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V_1 C_1
V : Type u'
inst_4 : Category.{v', u'} V
inst_5 : MonoidalCategory.{v', u'} V
C : Type u
inst_6 : Category.{v, u} C
inst_7 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    (eId V X : tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ X X)
have change : Eq.{v' + 1} (α :=
  tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
    @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
  ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
  (eId V (X.obj (P := P)) :
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
Tactic: change _ = eId V X.obj
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (goal)
Goal:
V_1 : Type u'
inst : Category.{v', u'} V_1
inst_1 : MonoidalCategory.{v', u'} V_1
C_1 : Type u
inst_2 : Category.{v, u} C_1
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V_1 C_1
V : Type u'
inst_4 : Category.{v', u'} V
inst_5 : MonoidalCategory.{v', u'} V
C : Type u
inst_6 : Category.{v, u} C
inst_7 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    (eId V (X.obj (P := P)) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
have rw : Eq.{v' + 1} (α :=
  tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
    @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
  ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
  ((eHomEquiv V : (a : X.obj ⟶ X.obj) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 (X.obj (P := P))) :
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
Tactic: rw [← eHomEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z : C
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
⊢ g = h
have w₁ : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
Tactic: replace w := se.section_ ≫= w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ Groupoid.{v₁, u₁} C
have all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), IsIso f
Tactic: apply Groupoid.ofIsIso
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
⊢ IsIso f
have a : IsSplitMono f
Tactic: have ⟨a,_⟩ := Trunc.exists_rep <| all_split_mono f
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
⊢ IsIso f
have h : sorry = sorry
Tactic: have ⟨a,_⟩ := Trunc.exists_rep <| all_split_mono f
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h : ⋯ = ⋯
⊢ IsIso f
have b : IsSplitMono (retraction f)
Tactic: have ⟨b,_⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h : ⋯ = ⋯
b : IsSplitMono (retraction f)
⊢ IsIso f
have h : sorry = sorry
Tactic: have ⟨b,_⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)
have rw : F.map (se.section_ ≫ f) = 𝟙 (F.obj Y)
Tactic: rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : Functor.{v₁, v₂, u₁, u₂} C D
rw : F.map (se.section_ ≫ f) = 𝟙 (F.obj Y)
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)
have rw₁ : F.map (𝟙 Y) = 𝟙 (F.obj Y)
Tactic: rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : Functor.{v₁, v₂, u₁, u₂} C D
rw : F.map (se.section_ ≫ f) = 𝟙 (F.obj Y)
rw₁ : F.map (𝟙 Y) = 𝟙 (F.obj Y)
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)
have rw₂ : Eq.{v₂ + 1} (α := F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y)) (𝟙 (F.obj Y))
Tactic: rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EpiMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
⊢ Epi (f ≫ g) ↔ Epi f
have refine : ∀ (h : Epi (f ≫ g)), Epi f
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X Y : C
p : X = Y
⊢ X ⟶ Y
have rw : Y ⟶ Y
Tactic: rw [p]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ Eq.{v₁ + 1} (α := X ⟶ Z) (eqToHom p ≫ eqToHom q) (eqToHom ⋯)
have refl : ∀ (q : X = Z), Eq.{v₁ + 1} (α := X ⟶ Z) (eqToHom sorry ≫ eqToHom q) (eqToHom sorry)
Tactic: cases p
Cleared hypotheses: Y, p, q
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
q : X = Z
⊢ Eq.{v₁ + 1} (α := X ⟶ Z) (eqToHom ⋯ ≫ eqToHom q) (eqToHom ⋯)
have refl : Eq.{v₁ + 1} (α := X ⟶ X) (eqToHom sorry ≫ eqToHom sorry) (eqToHom sorry)
Tactic: cases q
Cleared hypotheses: Z, q
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ HEq.{v₁ + 1} (α := X ⟶ Y) (eqToHom h) (β := X ⟶ X) (𝟙 X)
have subst : HEq.{v₁ + 1} (α := X ⟶ X) (eqToHom sorry) (β := X ⟶ X) (𝟙 X)
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ HEq.{v₁ + 1} (α := X ⟶ Y) (eqToHom h) (β := Y ⟶ Y) (𝟙 Y)
have subst : HEq.{v₁ + 1} (α := X ⟶ X) (eqToHom sorry) (β := X ⟶ X) (𝟙 X)
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ f = eqToHom h ≫ g ≫ eqToHom ⋯ ↔ f ≍ g
have refl : ∀ (g : W ⟶ Z), f = eqToHom sorry ≫ g ≫ eqToHom sorry ↔ f ≍ g
Tactic: cases h
Cleared hypotheses: Y, g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g
have refl : ∀ (g : W ⟶ X), f = eqToHom sorry ≫ g ≫ eqToHom sorry ↔ f ≍ g
Tactic: cases h'
Cleared hypotheses: Z, h', g
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y : C
f : Y ⟶ X
h : W = Y
⊢ eqToHom h ≫ f ≍ f
have rw : eqToHom h ≫ f = eqToHom h ≫ f ≫ eqToHom sorry
Tactic: rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ eqToHom h ≫ f ≍ f
have rw₁ : eqToHom h ≫ f = eqToHom h ≫ f ≫ 𝟙 X
Tactic: rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ eqToHom h ≫ f ≍ f
have rw₂ : eqToHom h ≫ f = eqToHom h ≫ f
Tactic: rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
h : Y = Z
⊢ f ≫ eqToHom h ≍ f
have rw : f ≫ eqToHom h = eqToHom sorry ≫ f ≫ eqToHom h
Tactic: rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ f ≫ eqToHom h ≍ f
have rw₁ : f ≫ eqToHom h = 𝟙 X ≫ f ≫ eqToHom h
Tactic: rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ f ≫ eqToHom h ≍ f
have rw₂ : f ≫ eqToHom h = f ≫ eqToHom h
Tactic: rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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'
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j'
have refl : z j ≫ eqToHom sorry = eqToHom sorry ≫ z j
Tactic: cases w
Cleared hypotheses: j', w
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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'
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').hom
have refl : (z j).hom ≫ eqToHom sorry = eqToHom sorry ≫ (z j).hom
Tactic: cases w
Cleared hypotheses: j', w
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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'
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').inv
have refl : (z j).inv ≫ eqToHom sorry = eqToHom sorry ≫ (z j).inv
Tactic: cases w
Cleared hypotheses: j', w
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ cast ⋯ q = eqToHom p ≫ q
have refl : ∀ (q : X ⟶ Z), cast sorry q = eqToHom sorry ≫ q
Tactic: cases p
Cleared hypotheses: Y, p, q
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ Eq.mpr ⋯ q = eqToHom p ≫ q
have refl : ∀ (q : X ⟶ Z), Eq.mpr sorry q = eqToHom sorry ≫ q
Tactic: cases p
Cleared hypotheses: Y, p, q
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ cast ⋯ p = p ≫ eqToHom ⋯
have refl : cast sorry p = p ≫ eqToHom sorry
Tactic: cases q
Cleared hypotheses: Z, q
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ Eq.mpr ⋯ p = p ≫ eqToHom ⋯
have refl : Eq.mpr sorry p = p ≫ eqToHom sorry
Tactic: cases q
Cleared hypotheses: Z, q
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ Eq.{v₁ + 1} (α := X ≅ Z) (eqToIso p ≪≫ eqToIso q) (eqToIso ⋯)
have w : Eq.{v₁ + 1} (α := X ⟶ Z) (Iso.hom (eqToIso p ≪≫ eqToIso q)) (Iso.hom (eqToIso sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op X) (Quiver.Hom.op (eqToHom h)) (eqToHom ⋯)
have refl : Eq.{v₁ + 1} (α := op X ⟶ op X) (Quiver.Hom.op (eqToHom sorry)) (eqToHom sorry)
Tactic: cases h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
h : X = Y
⊢ Eq.{v₁ + 1} (α := unop Y ⟶ unop X) (Quiver.Hom.unop (eqToHom h)) (eqToHom ⋯)
have refl : Eq.{v₁ + 1} (α := unop X ⟶ unop X) (Quiver.Hom.unop (eqToHom sorry)) (eqToHom sorry)
Tactic: cases h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ F_obj = G_obj
have h : ∀ (X : C), F_obj X = G_obj X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ { 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 }
have 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 sorry ≫
          { 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 sorry),
  { 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 }
Tactic: obtain rfl : F_obj = G_obj := by
      ext X
      apply h_obj
Cleared hypotheses: G_obj, map_1, map_id_1, map_comp_1, h_obj, h_map
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ { 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 }
have e_map : @map = @map_1
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ @map = @map_1
have e_map : ∀ (X Y : C) (f : X ⟶ Y), map f = map_1 f
Tactic: funext X Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw : F.map f ≫ e.hom.app Y = (eqToHom sorry ≫ G.map f ≫ eqToHom sorry) ≫ e.hom.app Y
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₁ : e.hom.app X ≫ G.map f = (eqToHom sorry ≫ G.map f ≫ eqToHom sorry) ≫ e.hom.app Y
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₂ : eqToHom sorry ≫ G.map f = (eqToHom sorry ≫ G.map f ≫ eqToHom sorry) ≫ e.hom.app Y
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₃ : eqToHom sorry ≫ G.map f = (eqToHom sorry ≫ G.map f ≫ eqToHom sorry) ≫ eqToHom sorry
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₄ : eqToHom sorry ≫ G.map f = eqToHom sorry ≫ (G.map f ≫ eqToHom sorry) ≫ eqToHom sorry
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]