Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
f : none ⟶ none
⊢ (F.map f ≫
      match none with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

pp: case none.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : none ⟶ some val✝
⊢ (F.map f ≫
      match some val✝ with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

pp: case some.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : some val✝ ⟶ none
⊢ (F.map f ≫
      match none with
      | none => f✝
      | some j => ι j) =
    (match some val✝ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

pp: case some.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ (F.map f ≫
      match some val✝ with
      | none => f✝
      | some j => ι j) =
    (match some val✝¹ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
<;>

Goal state after:
case none.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
f : none ⟶ none
⊢ (F.map f ≫
      match none with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

case none.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : none ⟶ some val✝
⊢ (F.map f ≫
      match some val✝ with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

case some.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : some val✝ ⟶ none
⊢ (F.map f ≫
      match none with
      | none => f✝
      | some j => ι j) =
    (match some val✝ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

case some.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ (F.map f ≫
      match some val✝ with
      | none => f✝
      | some j => ι j) =
    (match some val✝¹ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f