awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
leftCompReflexion : F.map (left ≫ reflexion) ≫ e₁ = e₁ ≫ G.map (left ≫ reflexion)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
⊢ F.map (left ≫ reflexion) ≫ e₁ = e₁ ≫ G.map (left ≫ reflexion)

Tactic:
simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
rightCompReflexion : F.map (right ≫ reflexion) ≫ e₁ = e₁ ≫ G.map (right ≫ reflexion)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
⊢ F.map (right ≫ reflexion) ≫ e₁ = e₁ ≫ G.map (right ≫ reflexion)

Tactic:
simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
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))
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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 (𝟙 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:
simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
⊢ (mkNatTrans e₀ e₁ h₁ h₂ h₃).app zero = e₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
⊢ (mkNatTrans e₀ e₁ h₁ h₂ h₃).app one = e₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
rw₄ rw₅ : F.map left = F.map left
⊢ G.map left ≫ e₀.inv = 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]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
rw₄ rw₅ : F.map right = F.map right
⊢ G.map right ≫ e₀.inv = 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]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
rw₄ rw₅ : F.map reflexion = F.map reflexion
⊢ G.map reflexion ≫ e₁.inv = 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]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
w :
  ∀ (x : WalkingReflexivePair),
    (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 F) x
⊢ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ = 𝟙 F

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
w₁ : (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app one = NatTrans.app (𝟙 F) one
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 F) x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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 ⋯ ⋯ ⋯).app zero = NatTrans.app (𝟙 F) zero

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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 ⋯ ⋯ ⋯).app one = NatTrans.app (𝟙 F) one

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
w :
  ∀ (x : WalkingReflexivePair),
    (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 G) x
⊢ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ = 𝟙 G

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
w₁ : (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app one = NatTrans.app (𝟙 G) one
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app x = NatTrans.app (𝟙 G) x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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 ⋯ ⋯ ⋯).app zero = NatTrans.app (𝟙 G) zero

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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 ⋯ ⋯ ⋯).app one = NatTrans.app (𝟙 G) one

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map s ≫ F.map f = 𝟙 (F.obj B)

Tactic:
simp only [← Functor.map_comp, sl, Functor.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map s ≫ F.map g = 𝟙 (F.obj B)

Tactic:
simp only [← Functor.map_comp, sr, Functor.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
⊢ (F ⋙ H).map left ≫ H.map e₀ = H.map e₁ ≫ (G ⋙ H).map left

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₁]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
⊢ (F ⋙ H).map right ≫ H.map e₀ = H.map e₁ ≫ (G ⋙ H).map right

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₂]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
⊢ (F ⋙ H).map reflexion ≫ H.map e₁ = H.map e₀ ≫ (G ⋙ H).map reflexion

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₃]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
w :
  ∀ (x : WalkingReflexivePair),
    (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app x = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) x
⊢ Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H = mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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
w :
  (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app zero =
    NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) zero
w₁ :
  (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app one = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) one
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app x = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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).app zero =
    NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) zero

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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).app one = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) one

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
⊢ IsReflexivePair (F.map left) (F.map right)

Tactic:
⟨F.map .reflexion, map_reflexion_comp_map_left F, map_reflexion_comp_map_right F⟩

Premises used: CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion, CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_left, CategoryTheory.Functor.map, And.intro, CategoryTheory.IsReflexivePair.mk, Exists.intro, CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
X : C
π : F.obj zero ⟶ X
h : F.map left ≫ π = F.map right ≫ π
⊢ (mk π h).π = π

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
rw : G.ι.app one = F.map right ≫ G.π
rw₁ rw₂ : G.ι.app one = G.ι.app one
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
rw [Cocone.w G left, Cocone.w G right]

Premises used: CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingReflexivePair.Hom.right, CategoryTheory.Limits.WalkingReflexivePair.Hom.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
⊢ G.ι.app zero = G.π

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
dsimp :
  ((Cocone.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
        (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).π =
    G.π
⊢ ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π

Tactic:
dsimp [reflexiveCoforkEquivCofork]

Premises used: CategoryTheory.Limits.reflexiveCoforkEquivCofork
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
⊢ ((Cocone.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
            (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).ι.app
      WalkingParallelPair.one =
    G.ι.app zero

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : Cofork (F.map left) (F.map right)
dsimp :
  NatTrans.app
      (Cocone.ι
        (Functor.obj (C :=
          Cocone.{0, v, 0, u} (J := WalkingParallelPair) (C := C)
            { obj := fun (X : WalkingParallelPair) ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
              map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
              map_id := ⋯, map_comp := ⋯ })
          Functor.Final.extendCocone
          { pt := G.pt,
            ι :=
              Iso.hom
                  (diagramIsoParallelPair
                    {
                      obj := fun (X : WalkingParallelPair) ↦
                        F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                      map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                        F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                      map_id := ⋯, map_comp := ⋯ }) ≫
                G.ι }))
      zero =
    G.π
⊢ ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π

Tactic:
dsimp only [reflexiveCoforkEquivCofork, Equivalence.symm, Equivalence.trans,
    ReflexiveCofork.π, Cocone.precomposeEquivalence, Cocone.precompose,
    Functor.comp, Functor.Final.coconesEquiv]

Premises used: CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.reflexiveCoforkEquivCofork, CategoryTheory.Functor.comp, CategoryTheory.Limits.Cocone.precomposeEquivalence, CategoryTheory.Equivalence.trans, CategoryTheory.Limits.ReflexiveCofork.π, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.Final.coconesEquiv