awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map Hom.left ≫ e₀ = e₁ ≫ G.map Hom.left
h₂ : F.map Hom.right ≫ e₀ = e₁ ≫ G.map Hom.right
h₃ : F.map Hom.reflexion ≫ e₁ = e₀ ≫ G.map Hom.reflexion
x x_1 : WalkingReflexivePair
f : x ⟶ x_1
left :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.left ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.left)
right :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.right ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.right)
reflexion :
  Eq (α := F.obj zero ⟶ G.obj one)
    (F.map Hom.reflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.reflexion)
leftCompReflexion :
  Eq (α := F.obj one ⟶ G.obj one)
    (F.map Hom.leftCompReflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.leftCompReflexion)
⊢ Eq (α := F.obj x ⟶ G.obj x_1)
    (F.map f ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x_1 with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁) ≫
      G.map f)
have rightCompReflexion : Eq (α := F.obj one ⟶ G.obj one)
  (F.map rightCompReflexion ≫
    match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
    | zero => e₀
    | one => e₁)
  ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
    | zero => e₀
    | one => e₁) ≫
    G.map rightCompReflexion)
Tactic: cases f
Cleared hypotheses: x, x_1, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map Hom.left ≫ e₀ = e₁ ≫ G.map Hom.left
h₂ : F.map Hom.right ≫ e₀ = e₁ ≫ G.map Hom.right
h₃ : F.map Hom.reflexion ≫ e₁ = e₀ ≫ G.map Hom.reflexion
x x_1 : WalkingReflexivePair
f : x ⟶ x_1
left :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.left ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.left)
right :
  Eq (α := F.obj one ⟶ G.obj zero)
    (F.map Hom.right ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.right)
reflexion :
  Eq (α := F.obj zero ⟶ G.obj one)
    (F.map Hom.reflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) zero with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.reflexion)
leftCompReflexion :
  Eq (α := F.obj one ⟶ G.obj one)
    (F.map Hom.leftCompReflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.leftCompReflexion)
rightCompReflexion :
  Eq (α := F.obj one ⟶ G.obj one)
    (F.map Hom.rightCompReflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map Hom.rightCompReflexion)
⊢ Eq (α := F.obj x ⟶ G.obj x_1)
    (F.map f ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x_1 with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁) ≫
      G.map f)
have id : Eq (α := F.obj x ⟶ G.obj x)
  (F.map (Hom.id x) ≫
    match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
    | zero => e₀
    | one => e₁)
  ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
    | zero => e₀
    | one => e₁) ≫
    G.map (Hom.id x))
Tactic: cases f
Cleared hypotheses: x_1, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ Eq (α := F.obj one ⟶ G.obj one)
    (F.map leftCompReflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map leftCompReflexion)
have leftCompReflexion : F.map (left ≫ reflexion) ≫ e₁ = e₁ ≫ G.map (left ≫ reflexion)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ Eq (α := F.obj one ⟶ G.obj one)
    (F.map rightCompReflexion ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) one with
      | zero => e₀
      | one => e₁) ≫
      G.map rightCompReflexion)
have rightCompReflexion : F.map (right ≫ reflexion) ≫ e₁ = e₁ ≫ G.map (right ≫ reflexion)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
x : WalkingReflexivePair
⊢ Eq (α := F.obj x ⟶ G.obj x)
    (F.map (Hom.id x) ≫
      match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁)
    ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
      | zero => e₀
      | one => e₁) ≫
      G.map (Hom.id x))
have id : Eq (α := F.obj x ⟶ G.obj x)
  (F.map (𝟙 x) ≫
    match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
    | zero => e₀
    | one => e₁)
  ((match (motive := (x : WalkingReflexivePair) → F.obj x ⟶ G.obj x) x with
    | zero => e₀
    | one => e₁) ≫
    G.map (𝟙 x))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ G.map left ≫ e₀.inv = e₁.inv ≫ F.map left
have rw : e₁.hom ≫ G.map left ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map left
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₁, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map left ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map left
⊢ G.map left ≫ e₀.inv = e₁.inv ≫ F.map left
have rw₁ : e₁.hom ≫ G.map left ≫ e₀.inv = F.map left
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₁, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map left ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map left
rw₁ : e₁.hom ≫ G.map left ≫ e₀.inv = F.map left
⊢ G.map left ≫ e₀.inv = e₁.inv ≫ F.map left
have rw₂ : F.map left ≫ e₀.hom ≫ e₀.inv = F.map left
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₁, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map left ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map left
rw₁ : e₁.hom ≫ G.map left ≫ e₀.inv = F.map left
rw₂ : F.map left ≫ e₀.hom ≫ e₀.inv = F.map left
⊢ G.map left ≫ e₀.inv = e₁.inv ≫ F.map left
have rw₃ : F.map left ≫ 𝟙 (F.obj zero) = F.map left
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₁, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map left ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map left
rw₁ : e₁.hom ≫ G.map left ≫ e₀.inv = F.map left
rw₂ : F.map left ≫ e₀.hom ≫ e₀.inv = F.map left
rw₃ : F.map left ≫ 𝟙 (F.obj zero) = F.map left
⊢ G.map left ≫ e₀.inv = e₁.inv ≫ F.map left
have rw₄ : F.map left = F.map left
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₁, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ G.map right ≫ e₀.inv = e₁.inv ≫ F.map right
have rw : e₁.hom ≫ G.map right ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map right
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₂, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map right ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map right
⊢ G.map right ≫ e₀.inv = e₁.inv ≫ F.map right
have rw₁ : e₁.hom ≫ G.map right ≫ e₀.inv = F.map right
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₂, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map right ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map right
rw₁ : e₁.hom ≫ G.map right ≫ e₀.inv = F.map right
⊢ G.map right ≫ e₀.inv = e₁.inv ≫ F.map right
have rw₂ : F.map right ≫ e₀.hom ≫ e₀.inv = F.map right
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₂, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map right ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map right
rw₁ : e₁.hom ≫ G.map right ≫ e₀.inv = F.map right
rw₂ : F.map right ≫ e₀.hom ≫ e₀.inv = F.map right
⊢ G.map right ≫ e₀.inv = e₁.inv ≫ F.map right
have rw₃ : F.map right ≫ 𝟙 (F.obj zero) = F.map right
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₂, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₁.hom ≫ G.map right ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map right
rw₁ : e₁.hom ≫ G.map right ≫ e₀.inv = F.map right
rw₂ : F.map right ≫ e₀.hom ≫ e₀.inv = F.map right
rw₃ : F.map right ≫ 𝟙 (F.obj zero) = F.map right
⊢ G.map right ≫ e₀.inv = e₁.inv ≫ F.map right
have rw₄ : F.map right = F.map right
Tactic: rw [← cancel_epi e₁.hom, e₁.hom_inv_id_assoc, ← reassoc_of% h₂, e₀.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ G.map reflexion ≫ e₁.inv = e₀.inv ≫ F.map reflexion
have rw : e₀.hom ≫ G.map reflexion ≫ e₁.inv = e₀.hom ≫ e₀.inv ≫ F.map reflexion
Tactic: rw [← cancel_epi e₀.hom, e₀.hom_inv_id_assoc, ← reassoc_of% h₃, e₁.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₀.hom ≫ G.map reflexion ≫ e₁.inv = e₀.hom ≫ e₀.inv ≫ F.map reflexion
⊢ G.map reflexion ≫ e₁.inv = e₀.inv ≫ F.map reflexion
have rw₁ : e₀.hom ≫ G.map reflexion ≫ e₁.inv = F.map reflexion
Tactic: rw [← cancel_epi e₀.hom, e₀.hom_inv_id_assoc, ← reassoc_of% h₃, e₁.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₀.hom ≫ G.map reflexion ≫ e₁.inv = e₀.hom ≫ e₀.inv ≫ F.map reflexion
rw₁ : e₀.hom ≫ G.map reflexion ≫ e₁.inv = F.map reflexion
⊢ G.map reflexion ≫ e₁.inv = e₀.inv ≫ F.map reflexion
have rw₂ : F.map reflexion ≫ e₁.hom ≫ e₁.inv = F.map reflexion
Tactic: rw [← cancel_epi e₀.hom, e₀.hom_inv_id_assoc, ← reassoc_of% h₃, e₁.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₀.hom ≫ G.map reflexion ≫ e₁.inv = e₀.hom ≫ e₀.inv ≫ F.map reflexion
rw₁ : e₀.hom ≫ G.map reflexion ≫ e₁.inv = F.map reflexion
rw₂ : F.map reflexion ≫ e₁.hom ≫ e₁.inv = F.map reflexion
⊢ G.map reflexion ≫ e₁.inv = e₀.inv ≫ F.map reflexion
have rw₃ : F.map reflexion ≫ 𝟙 (F.obj one) = F.map reflexion
Tactic: rw [← cancel_epi e₀.hom, e₀.hom_inv_id_assoc, ← reassoc_of% h₃, e₁.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
rw : e₀.hom ≫ G.map reflexion ≫ e₁.inv = e₀.hom ≫ e₀.inv ≫ F.map reflexion
rw₁ : e₀.hom ≫ G.map reflexion ≫ e₁.inv = F.map reflexion
rw₂ : F.map reflexion ≫ e₁.hom ≫ e₁.inv = F.map reflexion
rw₃ : F.map reflexion ≫ 𝟙 (F.obj one) = F.map reflexion
⊢ G.map reflexion ≫ e₁.inv = e₀.inv ≫ F.map reflexion
have rw₄ : F.map reflexion = F.map reflexion
Tactic: rw [← cancel_epi e₀.hom, e₀.hom_inv_id_assoc, ← reassoc_of% h₃, e₁.hom_inv_id,
            Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ = 𝟙 F
have w : ∀ (x : WalkingReflexivePair),
  (mkNatTrans e₀.hom e₁.hom sorry sorry sorry ≫ mkNatTrans e₀.inv e₁.inv sorry sorry sorry).app x = NatTrans.app (𝟙 F) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 F) x
have w : (mkNatTrans e₀.hom e₁.hom sorry sorry sorry ≫ mkNatTrans e₀.inv e₁.inv sorry sorry sorry).app zero = NatTrans.app (𝟙 F) zero
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
w : (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app zero = NatTrans.app (𝟙 F) zero
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 F) x
have w₁ : (mkNatTrans e₀.hom e₁.hom sorry sorry sorry ≫ mkNatTrans e₀.inv e₁.inv sorry sorry sorry).app one = NatTrans.app (𝟙 F) one
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ = 𝟙 G
have w : ∀ (x : WalkingReflexivePair),
  (mkNatTrans e₀.inv e₁.inv sorry sorry sorry ≫ mkNatTrans e₀.hom e₁.hom sorry sorry sorry).app x = NatTrans.app (𝟙 G) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 G) x
have w : (mkNatTrans e₀.inv e₁.inv sorry sorry sorry ≫ mkNatTrans e₀.hom e₁.hom sorry sorry sorry).app zero = NatTrans.app (𝟙 G) zero
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
w : (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app zero = NatTrans.app (𝟙 G) zero
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 G) x
have w₁ : (mkNatTrans e₀.inv e₁.inv sorry sorry sorry ≫ mkNatTrans e₀.hom e₁.hom sorry sorry sorry).app one = NatTrans.app (𝟙 G) one
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst_1 : Category.{v₂, u₂} D
H : Functor.{v, v₂, u, u₂} C D
⊢ Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H = mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯
have w : ∀ (x : WalkingReflexivePair),
  (Functor.whiskerRight (mkNatTrans e₀ e₁ sorry sorry sorry) H).app x = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) sorry sorry sorry) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst_1 : Category.{v₂, u₂} D
H : Functor.{v, v₂, u, u₂} C D
x : WalkingReflexivePair
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app x = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) x
have w : (Functor.whiskerRight (mkNatTrans e₀ e₁ sorry sorry sorry) H).app zero = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) sorry sorry sorry) zero
Tactic: cases x
Cleared hypotheses: x