awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (Quiver.Hom.unop (𝟙 Y) ≫ f.unop) = f
rw₁ : (𝟙 (unop Y) ≫ f.unop).op = f
rw₂ : f.unop.op = f
⊢ f ≫ 𝟙 Y = f
have rw₃ : f = f
Tactic: rw [← op_comp_unop, unop_id, id_comp, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsIso f.unop ↔ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
have rw : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop X)) (Y := op (unop Y)) f.unop.op ↔
  IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
Tactic: rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw :
  IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop X)) (Y := op (unop Y)) f.unop.op ↔
    IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ IsIso f.unop ↔ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
have rw₁ : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop X)) (Y := op (unop Y)) f ↔ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
Tactic: rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ (inv f).op = inv f.op
have hom_inv_id : Eq.{v₁ + 1} (α := op Y ⟶ op Y) (f.op ≫ (inv f).op) (𝟙 (op Y))
Tactic: apply IsIso.eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op Y) (f.op ≫ (inv f).op) (𝟙 (op Y))
have hom_inv_id : (inv f ≫ f).op = 𝟙 (op Y)
Tactic: rw [← op_comp, IsIso.inv_hom_id, op_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
hom_inv_id : (inv f ≫ f).op = 𝟙 (op Y)
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op Y) (f.op ≫ (inv f).op) (𝟙 (op Y))
have hom_inv_id₁ : Eq.{v₁ + 1} (α := op Y ⟶ op Y) (Quiver.Hom.op (𝟙 Y)) (𝟙 (op Y))
Tactic: rw [← op_comp, IsIso.inv_hom_id, op_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
hom_inv_id : (inv f ≫ f).op = 𝟙 (op Y)
hom_inv_id₁ : Eq.{v₁ + 1} (α := op Y ⟶ op Y) (Quiver.Hom.op (𝟙 Y)) (𝟙 (op Y))
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op Y) (f.op ≫ (inv f).op) (𝟙 (op Y))
have hom_inv_id₂ : Eq.{v₁ + 1} (α := op Y ⟶ op Y) (𝟙 (op Y)) (𝟙 (op Y))
Tactic: rw [← op_comp, IsIso.inv_hom_id, op_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ Quiver.Hom.unop (inv f) = inv f.unop
have hom_inv_id : f.unop ≫ Quiver.Hom.unop (inv f) = 𝟙 (unop Y)
Tactic: apply IsIso.eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ f.unop ≫ Quiver.Hom.unop (inv f) = 𝟙 (unop Y)
have hom_inv_id : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (inv f ≫ f)) (𝟙 (unop Y))
Tactic: rw [← unop_comp, IsIso.inv_hom_id, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
hom_inv_id : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (inv f ≫ f)) (𝟙 (unop Y))
⊢ f.unop ≫ Quiver.Hom.unop (inv f) = 𝟙 (unop Y)
have hom_inv_id₁ : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (𝟙 Y)) (𝟙 (unop Y))
Tactic: rw [← unop_comp, IsIso.inv_hom_id, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
hom_inv_id : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (inv f ≫ f)) (𝟙 (unop Y))
hom_inv_id₁ : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (𝟙 Y)) (𝟙 (unop Y))
⊢ f.unop ≫ Quiver.Hom.unop (inv f) = 𝟙 (unop Y)
have hom_inv_id₂ : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (𝟙 (unop Y)) (𝟙 (unop Y))
Tactic: rw [← unop_comp, IsIso.inv_hom_id, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
⊢ F.rightOp.leftOp = F
have mk : ∀ (obj : Cᵒᵖ → D) (map : {X Y : Cᵒᵖ} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : Cᵒᵖ), map (𝟙 X) = 𝟙 (obj X))
  (map_comp : ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D }.rightOp.leftOp =
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }
Tactic: cases F
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op = f
have w : f.unop.op.hom = f.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop = f
have w : f.op.unop.hom = f.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))
have rw : (e.inv.app X ≫ e.hom.app X).unop = 𝟙 (Opposite.unop (G.obj X))
Tactic: rw [← unop_comp, inv_hom_id_app, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
rw : (e.inv.app X ≫ e.hom.app X).unop = 𝟙 (Opposite.unop (G.obj X))
⊢ (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))
have rw₁ : Eq.{v_1 + 1} (α := Opposite.unop (G.obj X) ⟶ Opposite.unop (G.obj X)) (Quiver.Hom.unop (𝟙 (G.obj X)))
  (𝟙 (Opposite.unop (G.obj X)))
Tactic: rw [← unop_comp, inv_hom_id_app, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
rw : (e.inv.app X ≫ e.hom.app X).unop = 𝟙 (Opposite.unop (G.obj X))
rw₁ :
  Eq.{v_1 + 1} (α := Opposite.unop (G.obj X) ⟶ Opposite.unop (G.obj X)) (Quiver.Hom.unop (𝟙 (G.obj X)))
    (𝟙 (Opposite.unop (G.obj X)))
⊢ (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))
have rw₂ : Eq.{v_1 + 1} (α := Opposite.unop (G.obj X) ⟶ Opposite.unop (G.obj X)) (𝟙 (Opposite.unop (G.obj X)))
  (𝟙 (Opposite.unop (G.obj X)))
Tactic: rw [← unop_comp, inv_hom_id_app, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))
have rw : (e.hom.app X ≫ e.inv.app X).unop = 𝟙 (Opposite.unop (F.obj X))
Tactic: rw [← unop_comp, hom_inv_id_app, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
rw : (e.hom.app X ≫ e.inv.app X).unop = 𝟙 (Opposite.unop (F.obj X))
⊢ (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))
have rw₁ : Eq.{v_1 + 1} (α := Opposite.unop (F.obj X) ⟶ Opposite.unop (F.obj X)) (Quiver.Hom.unop (𝟙 (F.obj X)))
  (𝟙 (Opposite.unop (F.obj X)))
Tactic: rw [← unop_comp, hom_inv_id_app, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
rw : (e.hom.app X ≫ e.inv.app X).unop = 𝟙 (Opposite.unop (F.obj X))
rw₁ :
  Eq.{v_1 + 1} (α := Opposite.unop (F.obj X) ⟶ Opposite.unop (F.obj X)) (Quiver.Hom.unop (𝟙 (F.obj X)))
    (𝟙 (Opposite.unop (F.obj X)))
⊢ (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))
have rw₂ : Eq.{v_1 + 1} (α := Opposite.unop (F.obj X) ⟶ Opposite.unop (F.obj X)) (𝟙 (Opposite.unop (F.obj X)))
  (𝟙 (Opposite.unop (F.obj X)))
Tactic: rw [← unop_comp, hom_inv_id_app, unop_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
⊢ NatTrans.op α.hom ≫ NatTrans.op α.inv = 𝟙 G.op
have w : ∀ (x : Cᵒᵖ), (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x = NatTrans.app (𝟙 G.op) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
x : Cᵒᵖ
⊢ (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x = NatTrans.app (𝟙 G.op) x
have w : Eq.{v₂ + 1} (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x)))
  (Quiver.Hom.op (α.hom.app (unop x)) ≫ Quiver.Hom.op (α.inv.app (unop x))) (𝟙 (op (G.obj (unop x))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
x : Cᵒᵖ
⊢ Eq.{v₂ + 1} (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x)))
    (Quiver.Hom.op (α.hom.app (unop x)) ≫ Quiver.Hom.op (α.inv.app (unop x))) (𝟙 (op (G.obj (unop x))))
have w : Eq (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x))) (Quiver.Hom.op (α.inv.app (unop x) ≫ α.hom.app (unop x)))
  (𝟙 (op (G.obj (unop x))))
Tactic: rw [← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
x : Cᵒᵖ
⊢ Eq (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x))) (Quiver.Hom.op (α.inv.app (unop x) ≫ α.hom.app (unop x)))
    (𝟙 (op (G.obj (unop x))))
have w : Eq.{v₂ + 1} (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x))) (Quiver.Hom.op (𝟙 (G.obj (unop x))))
  (𝟙 (op (G.obj (unop x))))
Tactic: rw [α.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
⊢ NatTrans.op α.inv ≫ NatTrans.op α.hom = 𝟙 F.op
have w : ∀ (x : Cᵒᵖ), (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x = NatTrans.app (𝟙 F.op) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
x : Cᵒᵖ
⊢ (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x = NatTrans.app (𝟙 F.op) x
have w : Eq.{v₂ + 1} (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x)))
  (Quiver.Hom.op (α.inv.app (unop x)) ≫ Quiver.Hom.op (α.hom.app (unop x))) (𝟙 (op (F.obj (unop x))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
x : Cᵒᵖ
⊢ Eq.{v₂ + 1} (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x)))
    (Quiver.Hom.op (α.inv.app (unop x)) ≫ Quiver.Hom.op (α.hom.app (unop x))) (𝟙 (op (F.obj (unop x))))
have w : Eq (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x))) (Quiver.Hom.op (α.hom.app (unop x) ≫ α.inv.app (unop x)))
  (𝟙 (op (F.obj (unop x))))
Tactic: rw [← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ≅ G
x : Cᵒᵖ
⊢ Eq (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x))) (Quiver.Hom.op (α.hom.app (unop x) ≫ α.inv.app (unop x)))
    (𝟙 (op (F.obj (unop x))))
have w : Eq.{v₂ + 1} (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x))) (Quiver.Hom.op (𝟙 (F.obj (unop x))))
  (𝟙 (op (F.obj (unop x))))
Tactic: rw [α.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X : Cᵒᵖ
⊢ e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫ (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X) =
    𝟙 (e.functor.op.obj X)
have a : (e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫
      (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X)).unop =
  Quiver.Hom.unop (𝟙 (e.functor.op.obj X))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
X : C
⊢ e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
      (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X) =
    𝟙 (e.functor.unop.obj X)
have a : (e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
      (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X)).op =
  Quiver.Hom.op (𝟙 (e.functor.unop.obj X))
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 : F ⟶ G
⊢ Eq (α := obj (𝟭 (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) F ⟶ obj (opHom C D ⋙ opInv C D) G)
    (map (𝟭 (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) f ≫
      Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦ (unop F).opUnopIso.op) G))
    (Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦ (unop F).opUnopIso.op) F) ≫ map (opHom C D ⋙ opInv C D) f)
have dsimp : f ≫ (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) sorry).hom.op =
  (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) sorry).hom.op ≫
    Quiver.Hom.op { app := fun (X : C) ↦ f.unop.app X, naturality := sorry }
Tactic: dsimp [opUnopIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 : F ⟶ G
⊢ f ≫ (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) ⋯).hom.op =
    (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) ⋯).hom.op ≫
      Quiver.Hom.op { app := fun (X : C) ↦ f.unop.app X, naturality := ⋯ }
have rw : ((NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) sorry).hom ≫ f.unop).op =
  Quiver.Hom.op
    ({ app := fun (X : C) ↦ f.unop.op.unop.app X, naturality := sorry } ≫
      (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) sorry).hom)
Tactic: rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 : F ⟶ G
⊢ ((NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop).op =
    Quiver.Hom.op
      ({ app := fun (X : C) ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
        (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) ⋯).hom)
have e_f : (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) sorry).hom ≫ f.unop =
  { app := fun (X : C) ↦ f.unop.op.unop.app X, naturality := sorry } ≫
    (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) sorry).hom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ⟶ G
⊢ Eq (α :=
    obj (𝟭 (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) F ⟶
      obj
        (comp (D := Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ)
          { obj := fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOp,
            map := fun {X Y : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ} (η : X ⟶ Y) ↦ NatTrans.rightOp η.unop, map_id := ⋯,
            map_comp := ⋯ }
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ) ↦ op F.leftOp,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ} (η : X ⟶ Y) ↦ (NatTrans.leftOp η).op, map_id := ⋯,
            map_comp := ⋯ })
        G)
    (map (𝟭 (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) η ≫
      Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOpLeftOpIso.op) G))
    (Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOpLeftOpIso.op) F) ≫
      map
        (comp (D := Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ)
          { obj := fun (F : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ) ↦ (unop F).rightOp,
            map := fun {X Y : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ} (η : X ⟶ Y) ↦ NatTrans.rightOp η.unop, map_id := ⋯,
            map_comp := ⋯ : (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ }
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ) ↦ op F.leftOp,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ} (η : X ⟶ Y) ↦ (NatTrans.leftOp η).op, map_id := ⋯,
            map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ ⥤ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D)ᵒᵖ })
        η)
have dsimp : η ≫ (unop G).rightOpLeftOpIso.hom.op = (unop F).rightOpLeftOpIso.hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ⟶ G
⊢ η ≫ (unop G).rightOpLeftOpIso.hom.op =
    (unop F).rightOpLeftOpIso.hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op
have rw : ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
  (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op
Tactic: rw [show η = η.unop.op by simp, ← op_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (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 ⟶ G
⊢ ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op
have e_f : (unop G).rightOpLeftOpIso.hom ≫ η.unop =
  NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})) ↔
    Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
have mp : Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})) →
  Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
mp :
  Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})) →
    Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
⊢ Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})) ↔
    Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
have mpr : (Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))) →
  Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
have mp : (x y : C) → Unique (x ⟶ y)
Tactic: refine ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
⊢ x ⟶ y
have have : (hx : x ⟶ h.inverse.obj { as := PUnit.unit }) → x ⟶ y
Tactic: have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert! h.unit.app x
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y
have have : (hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y) → x ⟶ y
Tactic: have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert! h.unitInv.app y
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
⊢ Unique (x ⟶ y)
have mp : Subsingleton.{v + 1} (x ⟶ y)
Tactic: suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
⊢ Subsingleton.{v + 1} (x ⟶ y)
have this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
Tactic: have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y := by
      simp
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
⊢ Subsingleton.{v + 1} (x ⟶ y)
have mp : ∀ (a b : x ⟶ y), a = b
Tactic: apply Subsingleton.intro
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ a = b
have mp : h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
  h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y
Tactic: rw [this a, this b]
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y
have mp : h.unit.app x ≫ h.inverse.map (h.functor.map a) ≫ h.unitInv.app y =
  h.unit.app x ≫ h.inverse.map (h.functor.map b) ≫ h.unitInv.app y
Tactic: simp only [Functor.comp_map]