awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
J : Type u₅
inst_4 : Category.{v₅, u₅} J
K : Type u₆
inst_5 : Category.{v₆, u₆} K
Fₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
Gₗ : Functor.{v₃, v₅, u₃, u₅} E J
Gᵣ : Functor.{v₄, v₆, u₄, u₆} E' K
d : D
⊢ Eq (α := Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))
    (𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫
        𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫
          𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫ (mapPair Gₗ Gᵣ).map (𝟙 (right (Fᵣ.obj d))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))
    (𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
J : Type u₅
inst_4 : Category.{v₅, u₅} J
K : Type u₆
inst_5 : Category.{v₆, u₆} K
Fₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
Gₗ : Functor.{v₃, v₅, u₃, u₅} E J
Gᵣ : Functor.{v₄, v₆, u₄, u₆} E' K
c : C
dsimp :
  Eq (α := Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (left (Gₗ.obj (Fₗ.obj c))) (left (Gₗ.obj (Fₗ.obj c))))
    (((((mapPair Gₗ Gᵣ).map (𝟙 (left (Fₗ.obj c))) ≫ 𝟙 (left (Gₗ.obj (Fₗ.obj c)))) ≫ 𝟙 (left (Gₗ.obj (Fₗ.obj c)))) ≫
          𝟙 (left (Gₗ.obj (Fₗ.obj c)))) ≫
        𝟙 (left (Gₗ.obj (Fₗ.obj c))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (left (Gₗ.obj (Fₗ.obj c))) (left (Gₗ.obj (Fₗ.obj c))))
    (𝟙 (left (Gₗ.obj (Fₗ.obj c))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (left (Gₗ.obj (Fₗ.obj c))) (left (Gₗ.obj (Fₗ.obj c))))
⊢ Eq (α := (mapPair Fₗ Fᵣ ⋙ mapPair Gₗ Gᵣ).obj (left c) ⟶ (mapPair (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).obj (left c))
    ((mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (left c)) (𝟙 (left (Gₗ.obj (Fₗ.obj c))))

Tactic:
dsimp [mapPairComp]

Premises used: CategoryTheory.Join.mapPairComp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
J : Type u₅
inst_4 : Category.{v₅, u₅} J
K : Type u₆
inst_5 : Category.{v₆, u₆} K
Fₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
Gₗ : Functor.{v₃, v₅, u₃, u₅} E J
Gᵣ : Functor.{v₄, v₆, u₄, u₆} E' K
c : C
⊢ Eq (α := Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (left (Gₗ.obj (Fₗ.obj c))) (left (Gₗ.obj (Fₗ.obj c))))
    (((((mapPair Gₗ Gᵣ).map (𝟙 (left (Fₗ.obj c))) ≫ 𝟙 (left (Gₗ.obj (Fₗ.obj c)))) ≫ 𝟙 (left (Gₗ.obj (Fₗ.obj c)))) ≫
          𝟙 (left (Gₗ.obj (Fₗ.obj c)))) ≫
        𝟙 (left (Gₗ.obj (Fₗ.obj c))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (left (Gₗ.obj (Fₗ.obj c))) (left (Gₗ.obj (Fₗ.obj c))))
    (𝟙 (left (Gₗ.obj (Fₗ.obj c))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (left (Gₗ.obj (Fₗ.obj c))) (left (Gₗ.obj (Fₗ.obj c))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
J : Type u₅
inst_4 : Category.{v₅, u₅} J
K : Type u₆
inst_5 : Category.{v₆, u₆} K
Fₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
Gₗ : Functor.{v₃, v₅, u₃, u₅} E J
Gᵣ : Functor.{v₄, v₆, u₄, u₆} E' K
d : D
dsimp :
  Eq (α := Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))
    (((((mapPair Gₗ Gᵣ).map (𝟙 (right (Fᵣ.obj d))) ≫ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))) ≫ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))) ≫
          𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))) ≫
        𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))
    (𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))
⊢ Eq (α := (mapPair Fₗ Fᵣ ⋙ mapPair Gₗ Gᵣ).obj (right d) ⟶ (mapPair (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).obj (right d))
    ((mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (right d)) (𝟙 (right (Gᵣ.obj (Fᵣ.obj d))))

Tactic:
dsimp [mapPairComp]

Premises used: CategoryTheory.Join.mapPairComp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
J : Type u₅
inst_4 : Category.{v₅, u₅} J
K : Type u₆
inst_5 : Category.{v₆, u₆} K
Fₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
Gₗ : Functor.{v₃, v₅, u₃, u₅} E J
Gᵣ : Functor.{v₄, v₆, u₄, u₆} E' K
d : D
⊢ Eq (α := Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))
    (((((mapPair Gₗ Gᵣ).map (𝟙 (right (Fᵣ.obj d))) ≫ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))) ≫ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))) ≫
          𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))) ≫
        𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))
    (𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) :
      Quiver.Hom (V := Join.{v₅, v₆, u₅, u₆} J K) (right (Gᵣ.obj (Fᵣ.obj d))) (right (Gᵣ.obj (Fᵣ.obj d))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
Fₗ Gₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ Gᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
αₗ : Fₗ ⟶ Gₗ
αᵣ : Fᵣ ⟶ Gᵣ
w :
  ∀ (x : Join.{v₁, v₂, u₁, u₂} C D),
    (mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ).app x = (mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ).app x
⊢ mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ = mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
Fₗ Gₗ : Functor.{v₁, v₃, u₁, u₃} C E
α : Fₗ ≅ Gₗ
H : Functor.{v₂, v₄, u₂, u₄} D E'
⊢ (mapIsoWhiskerRight α H).hom = mapWhiskerRight α.hom H

Tactic:
rfl

Premises used: CategoryTheory.Join.mapWhiskerRight, CategoryTheory.Join.mkNatTrans, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
Fₗ Gₗ : Functor.{v₁, v₃, u₁, u₃} C E
α : Fₗ ≅ Gₗ
H : Functor.{v₂, v₄, u₂, u₄} D E'
w : ∀ (x : Join.{v₁, v₂, u₁, u₂} C D), (mapIsoWhiskerRight α H).inv.app x = (mapWhiskerRight α.inv H).app x
⊢ (mapIsoWhiskerRight α H).inv = mapWhiskerRight α.inv H

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
Fₗ Gₗ : Functor.{v₁, v₃, u₁, u₃} C E
α : Fₗ ≅ Gₗ
H : Functor.{v₂, v₄, u₂, u₄} D E'
x : Join.{v₁, v₂, u₁, u₂} C D
w :
  ∀ (a : C),
    Eq (α := (mapPair Gₗ H).obj (left a) ⟶ (mapPair Fₗ H).obj (left a)) ((mapIsoWhiskerRight α H).inv.app (left a))
      ((mapWhiskerRight α.inv H).app (left a))
w₁ :
  ∀ (a : D),
    Eq (α := (mapPair Gₗ H).obj (right a) ⟶ (mapPair Fₗ H).obj (right a)) ((mapIsoWhiskerRight α H).inv.app (right a))
      ((mapWhiskerRight α.inv H).app (right a))
⊢ (mapIsoWhiskerRight α H).inv.app x = (mapWhiskerRight α.inv H).app x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
Fₗ Gₗ : Functor.{v₁, v₃, u₁, u₃} C E
α : Fₗ ≅ Gₗ
H : Functor.{v₂, v₄, u₂, u₄} D E'
a : C
⊢ Eq (α := (mapPair Gₗ H).obj (left a) ⟶ (mapPair Fₗ H).obj (left a)) ((mapIsoWhiskerRight α H).inv.app (left a))
    ((mapWhiskerRight α.inv H).app (left a))

Tactic:
simp [mapIsoWhiskerRight]

Premises used: CategoryTheory.Join.mapIsoWhiskerRight
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
Fₗ Gₗ : Functor.{v₁, v₃, u₁, u₃} C E
α : Fₗ ≅ Gₗ
H : Functor.{v₂, v₄, u₂, u₄} D E'
a : D
⊢ Eq (α := (mapPair Gₗ H).obj (right a) ⟶ (mapPair Fₗ H).obj (right a)) ((mapIsoWhiskerRight α H).inv.app (right a))
    ((mapWhiskerRight α.inv H).app (right a))

Tactic:
simp [mapIsoWhiskerRight]

Premises used: CategoryTheory.Join.mapIsoWhiskerRight
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
H : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ Gᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
α : Fᵣ ≅ Gᵣ
⊢ (mapIsoWhiskerLeft H α).hom = mapWhiskerLeft H α.hom

Tactic:
rfl

Premises used: CategoryTheory.Join.mkNatTrans, CategoryTheory.Join.mapWhiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
H : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ Gᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
α : Fᵣ ≅ Gᵣ
w : ∀ (x : Join.{v₁, v₂, u₁, u₂} C D), (mapIsoWhiskerLeft H α).inv.app x = (mapWhiskerLeft H α.inv).app x
⊢ (mapIsoWhiskerLeft H α).inv = mapWhiskerLeft H α.inv

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
H : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ Gᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
α : Fᵣ ≅ Gᵣ
x : Join.{v₁, v₂, u₁, u₂} C D
w :
  ∀ (a : C),
    Eq (α := (mapPair H Gᵣ).obj (left a) ⟶ (mapPair H Fᵣ).obj (left a)) ((mapIsoWhiskerLeft H α).inv.app (left a))
      ((mapWhiskerLeft H α.inv).app (left a))
w₁ :
  ∀ (a : D),
    Eq (α := (mapPair H Gᵣ).obj (right a) ⟶ (mapPair H Fᵣ).obj (right a)) ((mapIsoWhiskerLeft H α).inv.app (right a))
      ((mapWhiskerLeft H α.inv).app (right a))
⊢ (mapIsoWhiskerLeft H α).inv.app x = (mapWhiskerLeft H α.inv).app x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
H : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ Gᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
α : Fᵣ ≅ Gᵣ
a : C
⊢ Eq (α := (mapPair H Gᵣ).obj (left a) ⟶ (mapPair H Fᵣ).obj (left a)) ((mapIsoWhiskerLeft H α).inv.app (left a))
    ((mapWhiskerLeft H α.inv).app (left a))

Tactic:
simp [mapIsoWhiskerLeft]

Premises used: CategoryTheory.Join.mapIsoWhiskerLeft
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
H : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ Gᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
α : Fᵣ ≅ Gᵣ
a : D
⊢ Eq (α := (mapPair H Gᵣ).obj (right a) ⟶ (mapPair H Fᵣ).obj (right a)) ((mapIsoWhiskerLeft H α).inv.app (right a))
    ((mapWhiskerLeft H α.inv).app (right a))

Tactic:
simp [mapIsoWhiskerLeft]

Premises used: CategoryTheory.Join.mapIsoWhiskerLeft
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
e' : Equivalence.{v₂, v₄, u₂, u₄} D D'
x : Join.{v₁, v₂, u₁, u₂} C D
left :
  ∀ (a : C),
    (mapPair e.functor e'.functor).map
          ((Iso.symm mapPairId ≪≫
                  mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                    mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                      mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
            (Join.left a)) ≫
        ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
                mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                  mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
          ((mapPair e.functor e'.functor).obj (Join.left a)) =
      𝟙 ((mapPair e.functor e'.functor).obj (Join.left a))
right :
  ∀ (a : D),
    (mapPair e.functor e'.functor).map
          ((Iso.symm mapPairId ≪≫
                  mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                    mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                      mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
            (Join.right a)) ≫
        ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
                mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                  mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
          ((mapPair e.functor e'.functor).obj (Join.right a)) =
      𝟙 ((mapPair e.functor e'.functor).obj (Join.right a))
⊢ (mapPair e.functor e'.functor).map
        ((Iso.symm mapPairId ≪≫
                mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                  mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                    mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
          x) ≫
      ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
              mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
        ((mapPair e.functor e'.functor).obj x) =
    𝟙 ((mapPair e.functor e'.functor).obj x)

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
e' : Equivalence.{v₂, v₄, u₂, u₄} D D'
a : C
⊢ (mapPair e.functor e'.functor).map
        ((Iso.symm mapPairId ≪≫
                mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                  mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                    mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
          (left a)) ≫
      ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
              mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
        ((mapPair e.functor e'.functor).obj (left a)) =
    𝟙 ((mapPair e.functor e'.functor).obj (left a))

Tactic:
simp [← (inclLeft C' D').map_comp, ← (inclRight C' D').map_comp]

Premises used: CategoryTheory.Join.inclLeft, CategoryTheory.Join.inclRight, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
e' : Equivalence.{v₂, v₄, u₂, u₄} D D'
a : D
⊢ (mapPair e.functor e'.functor).map
        ((Iso.symm mapPairId ≪≫
                mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                  mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                    mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
          (right a)) ≫
      ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
              mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
        ((mapPair e.functor e'.functor).obj (right a)) =
    𝟙 ((mapPair e.functor e'.functor).obj (right a))

Tactic:
simp [← (inclLeft C' D').map_comp, ← (inclRight C' D').map_comp]

Premises used: CategoryTheory.Join.inclLeft, CategoryTheory.Join.inclRight, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
F : Functor.{v₁, v₃, u₁, u₃} C C'
F' : Functor.{v₂, v₄, u₂, u₄} D D'
inst_4 : F.IsEquivalence
inst_5 : F'.IsEquivalence
⊢ (mapPair F F').IsEquivalence

Tactic:
inferInstanceAs (mapPairEquiv F.asEquivalence F'.asEquivalence).functor.IsEquivalence

Premises used: _private.0.CategoryTheory.Join.isEquivalenceMapPair._proof_1
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c : C
⊢ Eq (α := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ) (obj (Equivalence.functor (opEquiv C D)) (op (left c))) (right (op c))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
d : D
⊢ Eq (α := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ) (obj (Equivalence.functor (opEquiv C D)) (op (right d))) (left (op d))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c c' : C
f : c ⟶ c'
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ)
      (obj (Equivalence.functor (opEquiv C D)) (op ((inclLeft C D : C ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 c')))
      (obj (Equivalence.functor (opEquiv C D)) (op ((inclLeft C D : C ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 c))))
    (map (Equivalence.functor (opEquiv C D)) (op (map (inclLeft C D) f)) :
      Quiver.Hom (V := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ)
        (obj (Equivalence.functor (opEquiv C D)) (op ((inclLeft C D : C ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 c')))
        (obj (Equivalence.functor (opEquiv C D)) (op ((inclLeft C D : C ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 c))))
    (map (inclRight Dᵒᵖ Cᵒᵖ) (op f) :
      Quiver.Hom (V := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ) (obj (inclRight Dᵒᵖ Cᵒᵖ) (op c'))
        (obj (inclRight Dᵒᵖ Cᵒᵖ) (op c)))

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
d d' : D
f : d ⟶ d'
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ)
      (obj (Equivalence.functor (opEquiv C D)) (op ((inclRight C D : D ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 d')))
      (obj (Equivalence.functor (opEquiv C D)) (op ((inclRight C D : D ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 d))))
    (map (Equivalence.functor (opEquiv C D)) (op (map (inclRight C D) f)) :
      Quiver.Hom (V := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ)
        (obj (Equivalence.functor (opEquiv C D)) (op ((inclRight C D : D ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 d')))
        (obj (Equivalence.functor (opEquiv C D)) (op ((inclRight C D : D ⥤ Join.{v₁, v₂, u₁, u₂} C D).1 d))))
    (map (inclLeft Dᵒᵖ Cᵒᵖ) (op f) :
      Quiver.Hom (V := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ) (obj (inclLeft Dᵒᵖ Cᵒᵖ) (op d')) (obj (inclLeft Dᵒᵖ Cᵒᵖ) (op d)))

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c : C
d : D
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ) (obj (Equivalence.functor (opEquiv C D)) (op (right d)))
      (obj (Equivalence.functor (opEquiv C D)) (op (left c))))
    (map (Equivalence.functor (opEquiv C D)) (op (edge c d))) (edge (op d) (op c))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl, CategoryTheory.Join.edge
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
d : D
⊢ Eq (α := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (Equivalence.inverse (opEquiv C D)) (left (op d))) (op (right d))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c : C
⊢ Eq (α := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (Equivalence.inverse (opEquiv C D)) (right (op c))) (op (left c))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
d d' : D
f : d ⟶ d'
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ)
      (obj (Equivalence.inverse (opEquiv C D)) (obj (inclLeft Dᵒᵖ Cᵒᵖ) (op d')))
      (obj (Equivalence.inverse (opEquiv C D)) (obj (inclLeft Dᵒᵖ Cᵒᵖ) (op d))))
    (map (Equivalence.inverse (opEquiv C D)) (map (inclLeft Dᵒᵖ Cᵒᵖ) f.op)) (op (map (inclRight C D) f))

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c c' : C
f : c ⟶ c'
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ)
      (obj (Equivalence.inverse (opEquiv C D)) (obj (inclRight Dᵒᵖ Cᵒᵖ) (op c')))
      (obj (Equivalence.inverse (opEquiv C D)) (obj (inclRight Dᵒᵖ Cᵒᵖ) (op c))))
    (map (Equivalence.inverse (opEquiv C D)) (map (inclRight Dᵒᵖ Cᵒᵖ) f.op)) (op (map (inclLeft C D) f))

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c : C
d : D
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (Equivalence.inverse (opEquiv C D)) (left (op d)))
      (obj (Equivalence.inverse (opEquiv C D)) (right (op c))))
    (map (Equivalence.inverse (opEquiv C D)) (edge (op d) (op c))) (op (edge c d))

Tactic:
rfl

Premises used: Quiver.Hom.op, CategoryTheory.Join.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
d : D
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (inclLeft Dᵒᵖ Cᵒᵖ ⋙ Equivalence.inverse (opEquiv C D)) (op d))
      (obj (Functor.op (inclRight C D)) (op d)))
    (NatTrans.app (Iso.hom (inclLeftCompOpEquivInverse C D)) (op d)) (𝟙 (op (right d)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c : C
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (inclRight Dᵒᵖ Cᵒᵖ ⋙ Equivalence.inverse (opEquiv C D)) (op c))
      (obj (Functor.op (inclLeft C D)) (op c)))
    (NatTrans.app (Iso.hom (inclRightCompOpEquivInverse C D)) (op c)) (𝟙 (op (left c)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
d : D
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (Functor.op (inclRight C D)) (op d))
      (obj (inclLeft Dᵒᵖ Cᵒᵖ ⋙ Equivalence.inverse (opEquiv C D)) (op d)))
    (NatTrans.app (Iso.inv (inclLeftCompOpEquivInverse C D)) (op d)) (𝟙 (op (right d)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Join.Opposites
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
c : C
⊢ Eq (α :=
    Quiver.Hom (V := (Join.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) (obj (Functor.op (inclLeft C D)) (op c))
      (obj (inclRight Dᵒᵖ Cᵒᵖ ⋙ Equivalence.inverse (opEquiv C D)) (op c)))
    (NatTrans.app (Iso.inv (inclRightCompOpEquivInverse C D)) (op c)) (𝟙 (op (left c)))

Tactic:
rfl

Premises used: rfl