mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case 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✝
j' : WidePullbackShape J
f : none ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match none with
      | none => f✝
      | some j => π j) ≫
      F.map f

pp: case 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✝
j' : WidePullbackShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match some val✝ with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
<;>

Goal state after:
case 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✝
j' : WidePullbackShape J
f : none ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match none with
      | none => f✝
      | some j => π j) ≫
      F.map f

case 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✝
j' : WidePullbackShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match some val✝ with
      | none => f✝
      | some j => π j) ≫
      F.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.none.id
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
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id none) ≫
      match none with
      | none => f
      | some j => π j) =
    (match none with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id none)

pp: case some.none.term
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
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.term val✝) ≫
      match none with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.term val✝)

pp: case some.some.id
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
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id (some val✝)) ≫
      match some val✝ with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id (some val✝))

Tactic:
<;>

Goal state after:
case none.none.id
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
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id none) ≫
      match none with
      | none => f
      | some j => π j) =
    (match none with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id none)

case some.none.term
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
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.term val✝) ≫
      match none with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.term val✝)

case some.some.id
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
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id (some val✝)) ≫
      match some val✝ with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id (some val✝))
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePullbackShape J)).obj none ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePullbackShape J)).obj (some val✝) ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      (some val✝)

Tactic:
<;>

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePullbackShape J)).obj none ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePullbackShape J)).obj (some val✝) ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      none ≅
    (𝟭 (WidePullbackShape J')).obj none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      (some val✝) ≅
    (𝟭 (WidePullbackShape J')).obj (some val✝)

Tactic:
<;>

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      none ≅
    (𝟭 (WidePullbackShape J')).obj none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      (some val✝) ≅
    (𝟭 (WidePullbackShape J')).obj (some val✝)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
⊢ pre F E ≫ colim.map α = colim.map (E.whiskerLeft α) ≫ pre G E

Tactic:
ext
  rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X✝ : WidePullbackShape ι
⊢ F.map (Hom.id X✝) ≫
      (match X✝ with
        | none => base
        | some i => comp i).hom =
    (match X✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.id X✝)

pp: case term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
j✝ : ι
⊢ F.map (Hom.term j✝) ≫
      (match none with
        | none => base
        | some i => comp i).hom =
    (match some j✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.term j✝)

Tactic:
<;>

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X✝ : WidePullbackShape ι
⊢ F.map (Hom.id X✝) ≫
      (match X✝ with
        | none => base
        | some i => comp i).hom =
    (match X✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.id X✝)

case term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
j✝ : ι
⊢ F.map (Hom.term j✝) ≫
      (match none with
        | none => base
        | some i => comp i).hom =
    (match some j✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.term j✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case 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✝
j' : WidePushoutShape J
f : none ⟶ j'
⊢ (F.map f ≫
      match j' 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
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✝
j' : WidePushoutShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ (F.map f ≫
      match j' 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
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✝
j' : WidePushoutShape J
f : none ⟶ j'
⊢ (F.map f ≫
      match j' with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

case 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✝
j' : WidePushoutShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ (F.map f ≫
      match j' with
      | none => f✝
      | some j => ι j) =
    (match some val✝ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.none.id
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.map (Hom.id none) ≫
      match none with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id none)

pp: case none.some.init
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.map (Hom.init val✝) ≫
      match some val✝ with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.init val✝)

pp: case some.some.id
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.map (Hom.id (some val✝)) ≫
      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 (Hom.id (some val✝))

Tactic:
<;>

Goal state after:
case none.none.id
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.map (Hom.id none) ≫
      match none with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id none)

case none.some.init
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.map (Hom.init val✝) ≫
      match some val✝ with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.init val✝)

case some.some.id
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.map (Hom.id (some val✝)) ≫
      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 (Hom.id (some val✝))
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePushoutShape J)).obj none ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePushoutShape J)).obj (some val✝) ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      (some val✝)

Tactic:
<;>

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePushoutShape J)).obj none ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePushoutShape J)).obj (some val✝) ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      none ≅
    (𝟭 (WidePushoutShape J')).obj none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      (some val✝) ≅
    (𝟭 (WidePushoutShape J')).obj (some val✝)

Tactic:
<;>

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      none ≅
    (𝟭 (WidePushoutShape J')).obj none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      (some val✝) ≅
    (𝟭 (WidePushoutShape J')).obj (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        left) =
    left

pp: case right
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        right) =
    right

Tactic:
<;>

Goal state after:
case left
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        left) =
    left

case right
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        right) =
    right
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        left) =
    left

pp: case right
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        right) =
    right

Tactic:
<;>

Goal state after:
case left
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        left) =
    left

case right
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        right) =
    right
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case false
⊢ (fun x ↦
        match x with
        | left => true
        | right => false)
      ((fun b ↦ Bool.recOn b right left) false) =
    false

pp: case true
⊢ (fun x ↦
        match x with
        | left => true
        | right => false)
      ((fun b ↦ Bool.recOn b right left) true) =
    true

Tactic:
<;>

Goal state after:
case false
⊢ (fun x ↦
        match x with
        | left => true
        | right => false)
      ((fun b ↦ Bool.recOn b right left) false) =
    false

case true
⊢ (fun x ↦
        match x with
        | left => true
        | right => false)
      ((fun b ↦ Bool.recOn b right left) true) =
    true
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := left } = e.hom ≫ c'.π.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := right } = e.hom ≫ c'.π.app { as := right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := left } = e.hom ≫ c'.π.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := right } = e.hom ≫ c'.π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := left } ≫ e.hom = c'.ι.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := right } ≫ e.hom = c'.ι.app { as := right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := left } ≫ e.hom = c'.ι.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := right } ≫ e.hom = c'.ι.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst = lift (f ≫ g) (f ≫ h) ≫ fst

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd = lift (f ≫ g) (f ≫ h) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst = lift (f ≫ g) (f ≫ h) ≫ fst

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd = lift (f ≫ g) (f ≫ h) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ fst = 𝟙 (X ⨯ Y) ≫ fst

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ fst = 𝟙 (X ⨯ Y) ≫ fst

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd ≫ fst = 𝟙 (X ⨯ Y) ≫ fst

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd ≫ snd = 𝟙 (X ⨯ Y) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd ≫ fst = 𝟙 (X ⨯ Y) ≫ fst

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd ≫ snd = 𝟙 (X ⨯ Y) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ fst = lift (f ≫ h) (g ≫ k) ≫ fst

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ fst = lift (f ≫ h) (g ≫ k) ≫ fst

case h₂
C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ map h k) ≫ snd = lift (f ≫ h) (g ≫ k) ≫ snd