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 : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
f : none ⟶ none
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match none with
      | none => f✝
      | some j => π j) =
    (match none with
      | none => f✝
      | some j => π j) ≫
      F.map f

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

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

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

Tactic:
<;>

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

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

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

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