[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X✝ Y✝ Z✝ : C ⊕ D
X Y Z : C
x✝¹ : inl X ⟶ inl Y
x✝ : inl Y ⟶ inl Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inr X
            | inr X => inl X,
          map := fun X Y f =>
            match X, Y, f with
            | inl val, inl val_1, f => f
            | inr val, inr val_1, f => f }.map
      (x✝¹ ≫ x✝) =
    {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝¹ ≫
      {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X✝ Y✝ Z✝ : C ⊕ D
X Y Z : D
x✝¹ : inr X ⟶ inr Y
x✝ : inr Y ⟶ inr Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inr X
            | inr X => inl X,
          map := fun X Y f =>
            match X, Y, f with
            | inl val, inl val_1, f => f
            | inr val, inr val_1, f => f }.map
      (x✝¹ ≫ x✝) =
    {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝¹ ≫
      {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X : C ⊕ D
⊢ (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X
[PROOFSTEP]
cases X
[GOAL]
case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : C
⊢ (𝟭 (C ⊕ D)).obj (inl val✝) = (swap C D ⋙ swap D C).obj (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : D
⊢ (𝟭 (C ⊕ D)).obj (inr val✝) = (swap C D ⋙ swap D C).obj (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : C ⊕ D} (f : X ⟶ Y),
    (𝟭 (C ⊕ D)).map f ≫ ((fun X => eqToIso (_ : (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X)) Y).hom =
      ((fun X => eqToIso (_ : (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X)) X).hom ≫ (swap C D ⋙ swap D C).map f
[PROOFSTEP]
simp only [swap]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : C ⊕ D} (f : X ⟶ Y),
    (𝟭 (C ⊕ D)).map f ≫ (eqToIso (_ : (𝟭 (C ⊕ D)).obj Y = (swap C D ⋙ swap D C).obj Y)).hom =
      (eqToIso (_ : (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X)).hom ≫
        (Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f } ⋙
              Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f }).map
          f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inr
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : C
val_1 : D
f : inl val ⟶ inr val_1
⊢ f =
    match inr val, inl val_1,
      match inl val, inr val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : D
val_1 : C
f : inr val ⟶ inl val_1
⊢ f =
    match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f
[PROOFSTEP]
cases f
[GOAL]
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : D
val_1 : C
f : inr val ⟶ inl val_1
⊢ f =
    match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f
[PROOFSTEP]
cases f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X : D ⊕ C
⊢ (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X
[PROOFSTEP]
cases X
[GOAL]
case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : D
⊢ (swap D C ⋙ swap C D).obj (inl val✝) = (𝟭 (D ⊕ C)).obj (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : C
⊢ (swap D C ⋙ swap C D).obj (inr val✝) = (𝟭 (D ⊕ C)).obj (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : D ⊕ C} (f : X ⟶ Y),
    (swap D C ⋙ swap C D).map f ≫ ((fun X => eqToIso (_ : (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X)) Y).hom =
      ((fun X => eqToIso (_ : (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X)) X).hom ≫ (𝟭 (D ⊕ C)).map f
[PROOFSTEP]
simp only [swap]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : D ⊕ C} (f : X ⟶ Y),
    (Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f } ⋙
              Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f }).map
          f ≫
        (eqToIso (_ : (swap D C ⋙ swap C D).obj Y = (𝟭 (D ⊕ C)).obj Y)).hom =
      (eqToIso (_ : (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X)).hom ≫ (𝟭 (D ⊕ C)).map f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inr
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : D
val_1 : C
f : inl val ⟶ inr val_1
⊢ (match inr val, inl val_1,
      match inl val, inr val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f) =
    f
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : C
val_1 : D
f : inr val ⟶ inl val_1
⊢ (match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f) =
    f
[PROOFSTEP]
cases f
[GOAL]
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : C
val_1 : D
f : inr val ⟶ inl val_1
⊢ (match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f) =
    f
[PROOFSTEP]
cases f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ IsEquivalence (equivalence C D).functor
[PROOFSTEP]
infer_instance
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X : A ⊕ C
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (𝟙 X) =
    𝟙
      ({
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.obj
        X)
[PROOFSTEP]
cases X
[GOAL]
case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val✝ : A
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (𝟙 (inl val✝)) =
    𝟙
      ({
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.obj
        (inl val✝))
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val✝ : C
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (𝟙 (inr val✝)) =
    𝟙
      ({
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.obj
        (inr val✝))
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : A
⊢ F.map (𝟙 (inl val)) = 𝟙 (inl (F.obj val))
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ G.map (𝟙 (inr val)) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
erw [F.map_id]
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : A
⊢ 𝟙 (F.obj val) = 𝟙 (inl (F.obj val))
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ G.map (𝟙 (inr val)) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ G.map (𝟙 (inr val)) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
erw [G.map_id]
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ 𝟙 (G.obj val) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X✝ Y✝ Z✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (f ≫ g) =
    {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        f ≫
      {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        g
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X✝ Y✝ Z✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (f ≫ g) =
    {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        f ≫
      {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        g
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X✝ Y✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
X Y : A
f : inl X ⟶ inl Y
⊢ (Functor.sum F H).map f ≫
      (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inl Y) =
    (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inl X) ≫
      (Functor.sum G I).map f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X✝ Y✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
X Y : C
f : inr X ⟶ inr Y
⊢ (Functor.sum F H).map f ≫
      (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inr Y) =
    (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inr X) ≫
      (Functor.sum G I).map f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl
