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 : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a : D
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
        | left x => F.obj x
        | right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
        | left x => F.obj x
        | right x => G.obj x :
        E))
    (homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
            | left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | left x => F.obj x
            | right x => G.obj x :
            E))
        (fun (x x_1 : C) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : D) (g : x ⟶ x_1) ↦ G.map g) fun (c : C) (d : D) ↦
        α.app (c, d) (x := right a) (𝟙 (right a)) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | left x => F.obj x
          | right x => G.obj x :
          E))
    (𝟙
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
        | left x => F.obj x
        | right x => G.obj x) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) right a with
          | left x => F.obj x
          | right x => G.obj x :
          E))
have right : G.map (𝟙 a) = 𝟙 (G.obj a)
Tactic: dsimp only [id_right, homInduction_right]
-- 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
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
⊢ whiskerRight (edgeTransform C D) (mkFunctor F G α) = α
have w : ∀ (x : C × D), (whiskerRight (edgeTransform C D) (mkFunctor F G α)).app x = α.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 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
⊢ 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
      | left x => αₗ.app x
      | right x => αᵣ.app x)
    ((match (motive := (x : Join.{v₁, v₂, u₁, u₂} C D) → F.obj x ⟶ F'.obj x) x with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map f)
have 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
      | left x => αₗ.app x
      | 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
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map (map (inclLeft C D) 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)
Cleared hypotheses: x, y, f
-- 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 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
        | 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
        | right x => αᵣ.app x) ≫
        F'.map (map (inclLeft C D) f))
⊢ 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
      | 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
      | right x => αᵣ.app x) ≫
      F'.map f)
have 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
      | 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
      | right x => αᵣ.app x) ≫
      F'.map (map (inclRight C D) 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)
Cleared hypotheses: x, y, f
-- 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 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))
⊢ 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)
have edge : ∀ (c : C) (d : D),
  Eq (α := F.obj (Join.left c) ⟶ F'.obj (Join.right d))
    (F.map (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 (edge c d))
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)
Cleared hypotheses: x, y, f
-- 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
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) β)
⊢ α = β
have w : ∀ (t : Join.{v₁, v₂, u₁, u₂} C D), α.app t = β.app t
Tactic: ext t
-- 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
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
⊢ α.app t = β.app t
have w : ∀ (t : C), Eq (α := F.obj (left t) ⟶ F'.obj (left t)) (α.app (left t)) (β.app (left 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₂
Cleared hypotheses: t
-- 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
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))
⊢ α.app t = β.app t
have w₁ : ∀ (t : D), Eq (α := F.obj (right t) ⟶ F'.obj (right t)) (α.app (right t)) (β.app (right 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₂
Cleared hypotheses: t
-- 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
F F' : Join.{v₁, v₂, u₁, u₂} C D ⥤ E
α : F ⟶ F'
⊢ mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯ = α
have h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F')
  (whiskerLeft (inclLeft C D) (mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) sorry))
  (whiskerLeft (inclLeft C D) α)
Tactic: apply natTrans_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
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) α)
⊢ mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) ⋯ = α
have h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F')
  (whiskerLeft (inclRight C D) (mkNatTrans (whiskerLeft (inclLeft C D) α) (whiskerLeft (inclRight C D) α) sorry))
  (whiskerLeft (inclRight C D) α)
Tactic: apply natTrans_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
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''
⊢ mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯ = mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'
have h₁ : Eq (α := inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'') (whiskerLeft (inclLeft C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) sorry))
  (whiskerLeft (inclLeft C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))
Tactic: apply natTrans_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
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'))
⊢ mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯ = mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'
have h₂ : Eq (α := inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'') (whiskerLeft (inclRight C D) (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) sorry))
  (whiskerLeft (inclRight C D) (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'))
Tactic: apply natTrans_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 : 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) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv =
    whiskerLeft (Prod.fst C D) eₗ.inv ≫ whiskerRight (edgeTransform C D) F
have 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
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
⊢ 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.inv (isoWhiskerLeft (Prod.fst C D) eₗ) ≫ whiskerRight (edgeTransform C D) F =
  whiskerRight (edgeTransform C D) G ≫ whiskerLeft (Prod.snd C D) eᵣ.inv
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
⊢ 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.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ᵣ)
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ᵣ)
⊢ 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₃ : 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ᵣ)
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ᵣ)
⊢ 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₄ : 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ᵣ)
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ᵣ)
⊢ 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.inv (isoWhiskerLeft (Prod.snd C D) eᵣ) =
  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]