Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.edge
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
d✝ : D
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      ((inclLeft C D).map f✝ ≫ edge y✝ d✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclLeft C D).map f✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge y✝ d✝)

pp: case right.right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x✝ y✝¹ : D
f✝¹ : x✝ ⟶ y✝¹
y✝ : D
f✝ : y✝¹ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      ((inclRight C D).map f✝¹ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝¹) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)

pp: case edge.right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c✝ : C
d✝ y✝ : D
f✝ : d✝ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      (edge c✝ d✝ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge c✝ d✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)

Tactic:
· case left.edge f d => simpa using! (α.naturality <| (Prod.sectL _ d).map f).symm

Goal state after:
case right.right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x✝ y✝¹ : D
f✝¹ : x✝ ⟶ y✝¹
y✝ : D
f✝ : y✝¹ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      ((inclRight C D).map f✝¹ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝¹) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)

case edge.right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c✝ : C
d✝ y✝ : D
f✝ : d✝ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      (edge c✝ d✝ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge c✝ d✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)