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'
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
c : C
d : D
⊢ Eq (α := F.obj (left c) ⟶ F'.obj (right d))
    (F.map (edge c d) ≫
      match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) right d with
      | left x => αₗ.app x
      | right x => αᵣ.app x)
    ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) left c with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map (edge c d))

Tactic:
exact funext_iff.mp (NatTrans.ext_iff.mp h) (c, d)

Premises used: funext_iff, Prod.mk, Iff.mp, CategoryTheory.NatTrans.ext_iff
-- 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 F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
x y : Join.{v₁, v₂, u₁, u₂} C D
f : x ⟶ y
left :
  ∀ (x y : C) (f : x ⟶ y),
    Eq (α := F.obj (obj (inclLeft C D) x) ⟶ F'.obj (obj (inclLeft C D) y))
      (F.map (map (inclLeft C D) f) ≫
        match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclLeft C D) y with
        | Join.left x => αₗ.app x
        | Join.right x => αᵣ.app x)
      ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclLeft C D) x with
        | Join.left x => αₗ.app x
        | Join.right x => αᵣ.app x) ≫
        F'.map (map (inclLeft C D) f))
right :
  ∀ (x y : D) (f : x ⟶ y),
    Eq (α := F.obj (obj (inclRight C D) x) ⟶ F'.obj (obj (inclRight C D) y))
      (F.map (map (inclRight C D) f) ≫
        match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclRight C D) y with
        | Join.left x => αₗ.app x
        | Join.right x => αᵣ.app x)
      ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) obj (inclRight C D) x with
        | Join.left x => αₗ.app x
        | Join.right x => αᵣ.app x) ≫
        F'.map (map (inclRight C D) f))
edge :
  ∀ (c : C) (d : D),
    Eq (α := F.obj (Join.left c) ⟶ F'.obj (Join.right d))
      (F.map (Join.edge c d) ≫
        match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) Join.right d with
        | Join.left x => αₗ.app x
        | Join.right x => αᵣ.app x)
      ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) Join.left c with
        | Join.left x => αₗ.app x
        | Join.right x => αᵣ.app x) ≫
        F'.map (Join.edge c d))
⊢ Eq (α := F.obj x ⟶ F'.obj y)
    (F.map f ≫
      match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) y with
      | Join.left x => αₗ.app x
      | Join.right x => αᵣ.app x)
    ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) x with
      | Join.left x => αₗ.app x
      | Join.right x => αᵣ.app x) ≫
      F'.map f)

Tactic:
cases f with
    | @left x y f => simpa using αₗ.naturality f
    | @right x y f => simpa using αᵣ.naturality f
    | @edge c d => exact funext_iff.mp (NatTrans.ext_iff.mp h) (c, d)

Premises used: CategoryTheory.Join.left, CategoryTheory.Join.right, CategoryTheory.NatTrans.naturality, CategoryTheory.Join.edge
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
c : C
⊢ (mkNatTrans αₗ αᵣ h).app (left c) = αₗ.app c

Tactic:
rfl

Premises used: 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
d : D
⊢ (mkNatTrans αₗ αᵣ h).app (right d) = αᵣ.app d

Tactic:
rfl

Premises used: 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
⊢ whiskerLeft (inclLeft C D) (mkNatTrans αₗ αᵣ h) = αₗ

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
⊢ whiskerLeft (inclRight C D) (mkNatTrans αₗ αᵣ h) = αᵣ

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α β : F ⟶ F'
h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclLeft C D) β)
h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F') (whiskerLeft (inclRight C D) α) (whiskerLeft (inclRight C D) β)
w : ∀ (t : Join.{v₁, v₂, u₁, u₂} C D), α.app t = β.app t
⊢ α = β

Tactic:
ext t
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α β : F ⟶ F'
h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclLeft C D) β)
h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F') (whiskerLeft (inclRight C D) α) (whiskerLeft (inclRight C D) β)
t : C
⊢ Eq (α := F.obj (left t) ⟶ F'.obj (left t)) (α.app (left t)) (β.app (left t))

Tactic:
congrArg (fun x ↦ x.app t) h₁

Premises used: congrArg
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α β : F ⟶ F'
h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclLeft C D) β)
h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F') (whiskerLeft (inclRight C D) α) (whiskerLeft (inclRight C D) β)
t : C
⊢ Eq (α := F.obj (left t) ⟶ F'.obj (left t)) (α.app (left t)) (β.app (left t))

Tactic:
exact congrArg (fun x ↦ x.app t) h₁

Premises used: congrArg
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α β : F ⟶ F'
h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclLeft C D) β)
h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F') (whiskerLeft (inclRight C D) α) (whiskerLeft (inclRight C D) β)
t : D
⊢ Eq (α := F.obj (right t) ⟶ F'.obj (right t)) (α.app (right t)) (β.app (right t))

Tactic:
congrArg (fun x ↦ x.app t) h₂

Premises used: congrArg
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α β : F ⟶ F'
h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclLeft C D) β)
h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F') (whiskerLeft (inclRight C D) α) (whiskerLeft (inclRight C D) β)
t : D
⊢ Eq (α := F.obj (right t) ⟶ F'.obj (right t)) (α.app (right t)) (β.app (right t))

Tactic:
exact congrArg (fun x ↦ x.app t) h₂

Premises used: congrArg
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α β : F ⟶ F'
h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclLeft C D) β)
h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F') (whiskerLeft (inclRight C D) α) (whiskerLeft (inclRight C D) β)
t : Join.{v₁, v₂, u₁, u₂} C D
w : ∀ (t : C), Eq (α := F.obj (left t) ⟶ F'.obj (left t)) (α.app (left t)) (β.app (left t))
w₁ : ∀ (t : D), Eq (α := F.obj (right t) ⟶ F'.obj (right t)) (α.app (right t)) (β.app (right t))
⊢ α.app t = β.app t

Tactic:
cases t with
  | left t => exact congrArg (fun x ↦ x.app t) h₁
  | right t => exact congrArg (fun x ↦ x.app t) h₂

Premises used: congrArg, CategoryTheory.Join.left, CategoryTheory.Join.right
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α : F ⟶ F'
h₁ :
  Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F')
    (whiskerLeft (inclLeft C D) (mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯))
    (whiskerLeft (inclLeft C D) α)
h₂ :
  Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F')
    (whiskerLeft (inclRight C D) (mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯))
    (whiskerLeft (inclRight C D) α)
⊢ mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯ = α

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Join.natTrans_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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α : F ⟶ F'
⊢ Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F')
    (whiskerLeft (inclLeft C D) (mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯))
    (whiskerLeft (inclLeft C 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α : F ⟶ F'
⊢ Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F')
    (whiskerLeft (inclRight C D) (mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯))
    (whiskerLeft (inclRight C 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 F' F'' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  autoParam
    (whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
      whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F')
    mkNatTransComp._auto_1
h' :
  autoParam
    (whiskerRight (edgeTransform C D) F' ≫ whiskerLeft (Prod.snd C D) βᵣ =
      whiskerLeft (Prod.fst C D) βₗ ≫ whiskerRight (edgeTransform C D) F'')
    mkNatTransComp._auto_2
⊢ whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) (αᵣ ≫ βᵣ) =
    whiskerLeft (Prod.fst C D) (αₗ ≫ βₗ) ≫ whiskerRight (edgeTransform C D) F''

Tactic:
simp [← h', reassoc_of% h]
-- 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
F F' F'' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ whiskerLeft (Prod.snd C D) βᵣ =
    whiskerLeft (Prod.fst C D) βₗ ≫ whiskerRight (edgeTransform C D) F''
h₁ :
  Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'') (whiskerLeft (inclLeft C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯))
    (whiskerLeft (inclLeft C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))
h₂ :
  Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'') (whiskerLeft (inclRight C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯))
    (whiskerLeft (inclRight C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))
⊢ mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯ = mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Join.natTrans_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
F F' F'' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ whiskerLeft (Prod.snd C D) βᵣ =
    whiskerLeft (Prod.fst C D) βₗ ≫ whiskerRight (edgeTransform C D) F''
h₁ h₂ h₃ h₄ :
  Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'') (whiskerLeft (inclLeft C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯))
    (whiskerLeft (inclLeft C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))
⊢ Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'') (whiskerLeft (inclLeft C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯))
    (whiskerLeft (inclLeft C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))

Tactic:
cat_disch
-- 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
F F' F'' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
    whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ whiskerLeft (Prod.snd C D) βᵣ =
    whiskerLeft (Prod.fst C D) βₗ ≫ whiskerRight (edgeTransform C D) F''
h₂ h₃ h₄ h₅ :
  Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'') (whiskerLeft (inclRight C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯))
    (whiskerLeft (inclRight C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))
⊢ Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'') (whiskerLeft (inclRight C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯))
    (whiskerLeft (inclRight C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))

Tactic:
cat_disch
-- 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 : 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
⊢ whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) eᵣ.hom =
    whiskerLeft (Prod.fst C D) eₗ.hom ≫ whiskerRight (edgeTransform C D) G

Tactic:
simpa using h
-- 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 : 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ᵣ)
rw₇ 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
⊢ whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv =
    whiskerLeft (Prod.fst C D) eₗ.inv ≫ whiskerRight (edgeTransform C D) F

Tactic:
rw [Eq.comm, ← isoWhiskerLeft_inv, ← isoWhiskerLeft_inv,
    Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Functor.isoWhiskerLeft_inv, Eq.comm
-- 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ₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
c : C
⊢ (mapPair Fₗ Fᵣ).obj (left c) = left (Fₗ.obj c)

Tactic:
rfl

Premises used: 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ₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
d : D
⊢ (mapPair Fₗ Fᵣ).obj (right d) = right (Fᵣ.obj d)

Tactic:
rfl

Premises used: 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ₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
c c' : C
f : c ⟶ c'
⊢ Eq (α := (mapPair Fₗ Fᵣ).obj (obj (inclLeft C D) c) ⟶ (mapPair Fₗ Fᵣ).obj (obj (inclLeft C D) c'))
    ((mapPair Fₗ Fᵣ).map (map (inclLeft C D) f)) (map (inclLeft E E') (Fₗ.map f))

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, 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ₗ : Functor.{v₁, v₃, u₁, u₃} C E
Fᵣ : Functor.{v₂, v₄, u₂, u₄} D E'
d d' : D
f : d ⟶ d'
⊢ Eq (α := (mapPair Fₗ Fᵣ).obj (obj (inclRight C D) d) ⟶ (mapPair Fₗ Fᵣ).obj (obj (inclRight C D) d'))
    ((mapPair Fₗ Fᵣ).map (map (inclRight C D) f)) (map (inclRight E E') (Fᵣ.map f))

Tactic:
rfl

Premises used: CategoryTheory.Join.homInduction, 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'
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))))
    (𝟙 (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))))
⊢ 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))))

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))))
    (𝟙 (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:
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))))
    (𝟙 (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))))
⊢ 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))))

Tactic:
dsimp [mapPairComp]

Premises used: CategoryTheory.Join.mapPairComp