awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ Iso.hom (isoWhiskerLeft (Prod.snd C D) eᵣ) =
    Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G
rw :
  whiskerLeft (Prod.fst C D) eₗ.inv ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv
rw₁ :
  Iso.inv (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv
rw₂ :
  Iso.inv (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ)
rw₃ :
  whiskerRight (edgeTransform C D) F =
    Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫
      whiskerRight (edgeTransform C D) G ≫ Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ)
rw₄ :
  whiskerRight (edgeTransform C D) F =
    (Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G) ≫
      Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ)
rw₅ :
  (Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G) ≫
      Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ) =
    whiskerRight (edgeTransform C D) F
⊢ whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv =
    whiskerLeft (Prod.fst C D) eₗ.inv ≫ whiskerRight (edgeTransform C D) F
have rw₆ : Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G =
  whiskerRight (edgeTransform C D) F ≫ Iso.hom (isoWhiskerLeft (Prod.snd C D) eᵣ)
Tactic: rw [Eq.comm, ← isoWhiskerLeft_inv, ← isoWhiskerLeft_inv,
    Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ Iso.hom (isoWhiskerLeft (Prod.snd C D) eᵣ) =
    Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G
rw :
  whiskerLeft (Prod.fst C D) eₗ.inv ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv
rw₁ :
  Iso.inv (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv
rw₂ :
  Iso.inv (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ)
rw₃ :
  whiskerRight (edgeTransform C D) F =
    Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫
      whiskerRight (edgeTransform C D) G ≫ Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ)
rw₄ :
  whiskerRight (edgeTransform C D) F =
    (Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G) ≫
      Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ)
rw₅ :
  (Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G) ≫
      Iso.inv (isoWhiskerLeft (Prod.snd C D) eᵣ) =
    whiskerRight (edgeTransform C D) F
rw₆ :
  Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G =
    whiskerRight (edgeTransform C D) F ≫ Iso.hom (isoWhiskerLeft (Prod.snd C D) eᵣ)
⊢ whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv =
    whiskerLeft (Prod.fst C D) eₗ.inv ≫ whiskerRight (edgeTransform C D) F
have rw₇ : Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G =
  Iso.hom (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) G
Tactic: rw [Eq.comm, ← isoWhiskerLeft_inv, ← isoWhiskerLeft_inv,
    Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 (α := (mapPair (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).obj (left c) ⟶ (mapPair Fₗ Fᵣ ⋙ mapPair Gₗ Gᵣ).obj (left c))
    ((mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (left c)) (𝟙 (left (Gₗ.obj (Fₗ.obj c))))
have dsimp : Eq (α := 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))) ≫
      𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫
        𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫ 𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫ (mapPair Gₗ Gᵣ).map (𝟙 (left (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: dsimp [mapPairComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 (α := (mapPair (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).obj (right d) ⟶ (mapPair Fₗ Fᵣ ⋙ mapPair Gₗ Gᵣ).obj (right d))
    ((mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (right d)) (𝟙 (right (Gᵣ.obj (Fᵣ.obj d))))
have dsimp : 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: dsimp [mapPairComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 (α := (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))))
have 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))))
Tactic: dsimp [mapPairComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 (α := (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))))
have 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))))
Tactic: dsimp [mapPairComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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ᵣ
⊢ mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ = mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ
have w : ∀ (x : Join.{v₁, v₂, u₁, u₂} C D),
  (mapWhiskerLeft Fₗ αᵣ ≫ mapWhiskerRight αₗ Gᵣ).app x = (mapWhiskerRight αₗ Fᵣ ≫ mapWhiskerLeft Gₗ αᵣ).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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).inv = mapWhiskerRight α.inv H
have w : ∀ (x : Join.{v₁, v₂, u₁, u₂} C D), (mapIsoWhiskerRight α H).inv.app x = (mapWhiskerRight α.inv H).app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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
⊢ (mapIsoWhiskerRight α H).inv.app x = (mapWhiskerRight α.inv H).app x
have 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))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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))
⊢ (mapIsoWhiskerRight α H).inv.app x = (mapWhiskerRight α.inv H).app x
have 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))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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 α).inv = mapWhiskerLeft H α.inv
have w : ∀ (x : Join.{v₁, v₂, u₁, u₂} C D), (mapIsoWhiskerLeft H α).inv.app x = (mapWhiskerLeft H α.inv).app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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
⊢ (mapIsoWhiskerLeft H α).inv.app x = (mapWhiskerLeft H α.inv).app x
have 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))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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))
⊢ (mapIsoWhiskerLeft H α).inv.app x = (mapWhiskerLeft H α.inv).app x
have 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))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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
⊢ (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)
have 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
          (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: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
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))
⊢ (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)
have 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
          (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: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} A B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (mapPair (𝟭 A) (F ⋙ G))
      (mapPair (𝟭 A) (F ⋙ H)))
    (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))
    (Iso.hom (mapCompRight A F G) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H))
have h₁ : Eq (α :=
  Quiver.Hom (V := A ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G))
    (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
  (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
  (Functor.whiskerLeft (inclLeft A B)
    (Iso.hom (mapCompRight A F G) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
h₁ :
  Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G))
      (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F G) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} A B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (mapPair (𝟭 A) (F ⋙ G))
      (mapPair (𝟭 A) (F ⋙ H)))
    (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))
    (Iso.hom (mapCompRight A F G) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H))
have h₂ : Eq (α :=
  Quiver.Hom (V := B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G))
    (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
  (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
  (Functor.whiskerLeft (inclRight A B)
    (Iso.hom (mapCompRight A F G) ≫
      Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
⊢ Eq (α :=
    Quiver.Hom (V := A ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G))
      (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
    (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
    (Functor.whiskerLeft (inclLeft A B)
      (Iso.hom (mapCompRight A F G) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
have h₁ : ∀ (x : A),
  Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ G)) x)
      (obj (inclLeft A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclLeft A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclLeft A B)
        (Iso.hom (mapCompRight A F G) ≫
          Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_3, u_2, u_3} B C
G H : Functor.{v_3, v_4, u_3, u_4} C D
η : G ⟶ H
⊢ Eq (α :=
    Quiver.Hom (V := B ⥤ Join.{v_1, v_4, u_1, u_4} A D) (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G))
      (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)))
    (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η)))
    (Functor.whiskerLeft (inclRight A B)
      (Iso.hom (mapCompRight A F G) ≫
        Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
have h₂ : ∀ (x : B),
  Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D) (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ G)) x)
      (obj (inclRight A B ⋙ mapPair (𝟭 A) (F ⋙ H)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A B) (mapWhiskerLeft (𝟭 A) (F.whiskerLeft η))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A B)
        (Iso.hom (mapCompRight A F G) ≫
          Functor.whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft (𝟭 A) η) ≫ Iso.inv (mapCompRight A F H)))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_1, v_2, u_1, u_2} A B
G H : Functor.{v_2, v_3, u_2, u_3} B C
η : G ⟶ H
⊢ Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_4, u_1, u_4} A D ⥤ Join.{v_3, v_4, u_3, u_4} C D) (mapPair (F ⋙ G) (𝟭 D))
      (mapPair (F ⋙ H) (𝟭 D)))
    (mapWhiskerRight (F.whiskerLeft η) (𝟭 D))
    (Iso.hom (mapCompLeft D F G) ≫
      Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H))
have h₁ : Eq (α :=
  Quiver.Hom (V := A ⥤ Join.{v_3, v_4, u_3, u_4} C D) (inclLeft A D ⋙ mapPair (F ⋙ G) (𝟭 D))
    (inclLeft A D ⋙ mapPair (F ⋙ H) (𝟭 D)))
  (Functor.whiskerLeft (inclLeft A D) (mapWhiskerRight (F.whiskerLeft η) (𝟭 D)))
  (Functor.whiskerLeft (inclLeft A D)
    (Iso.hom (mapCompLeft D F G) ≫
      Functor.whiskerLeft (mapPair F (𝟭 D)) (mapWhiskerRight η (𝟭 D)) ≫ Iso.inv (mapCompLeft D F H)))
Tactic: apply natTrans_ext