mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
x✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).f x✝ = (U.powerπ (f a)).f x✝

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
i✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).φ i✝ ≫ eqToHom ⋯ = (U.powerπ (f a)).φ i✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
x✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).f x✝ = (U.powerπ (f a)).f x✝

case h₂
C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
i✝ : (U.power β).I
⊢ (U.mapPower f ≫ U.powerπ a).φ i✝ ≫ eqToHom ⋯ = (U.powerπ (f a)).φ i✝
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclLeft C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclLeft C D).whiskerLeft α

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclRight C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclRight C D).whiskerLeft α

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclLeft C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclLeft C D).whiskerLeft α

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclRight C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclRight C D).whiskerLeft α
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' F'' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ (Prod.snd C D).whiskerLeft βᵣ =
    (Prod.fst C D).whiskerLeft βₗ ≫ whiskerRight (edgeTransform C D) F''
⊢ (inclLeft C D).whiskerLeft (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯) =
    (inclLeft C D).whiskerLeft (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h')

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' F'' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ (Prod.snd C D).whiskerLeft βᵣ =
    (Prod.fst C D).whiskerLeft βₗ ≫ whiskerRight (edgeTransform C D) F''
⊢ (inclRight C D).whiskerLeft (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯) =
    (inclRight C D).whiskerLeft (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h')

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' F'' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ (Prod.snd C D).whiskerLeft βᵣ =
    (Prod.fst C D).whiskerLeft βₗ ≫ whiskerRight (edgeTransform C D) F''
⊢ (inclLeft C D).whiskerLeft (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯) =
    (inclLeft C D).whiskerLeft (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h')

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' F'' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ (Prod.snd C D).whiskerLeft βᵣ =
    (Prod.fst C D).whiskerLeft βₗ ≫ whiskerRight (edgeTransform C D) F''
⊢ (inclRight C D).whiskerLeft (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯) =
    (inclRight C D).whiskerLeft (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h')
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left
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ₗ Gₗ : C ⥤ E
α : Fₗ ≅ Gₗ
H : D ⥤ E'
a✝ : C
⊢ (mapIsoWhiskerRight α H).inv.app (left a✝) = (mapWhiskerRight α.inv H).app (left a✝)

pp: case 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ₗ Gₗ : C ⥤ E
α : Fₗ ≅ Gₗ
H : D ⥤ E'
a✝ : D
⊢ (mapIsoWhiskerRight α H).inv.app (right a✝) = (mapWhiskerRight α.inv H).app (right a✝)

Tactic:
<;>

Goal state after:
case left
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ₗ Gₗ : C ⥤ E
α : Fₗ ≅ Gₗ
H : D ⥤ E'
a✝ : C
⊢ (mapIsoWhiskerRight α H).inv.app (left a✝) = (mapWhiskerRight α.inv H).app (left a✝)

case 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ₗ Gₗ : C ⥤ E
α : Fₗ ≅ Gₗ
H : D ⥤ E'
a✝ : D
⊢ (mapIsoWhiskerRight α H).inv.app (right a✝) = (mapWhiskerRight α.inv H).app (right a✝)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left
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'
H : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
α : Fᵣ ≅ Gᵣ
a✝ : C
⊢ (mapIsoWhiskerLeft H α).inv.app (left a✝) = (mapWhiskerLeft H α.inv).app (left a✝)

pp: case 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'
H : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
α : Fᵣ ≅ Gᵣ
a✝ : D
⊢ (mapIsoWhiskerLeft H α).inv.app (right a✝) = (mapWhiskerLeft H α.inv).app (right a✝)

Tactic:
<;>

Goal state after:
case left
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'
H : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
α : Fᵣ ≅ Gᵣ
a✝ : C
⊢ (mapIsoWhiskerLeft H α).inv.app (left a✝) = (mapWhiskerLeft H α.inv).app (left a✝)

case 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'
H : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
α : Fᵣ ≅ Gᵣ
a✝ : D
⊢ (mapIsoWhiskerLeft H α).inv.app (right a✝) = (mapWhiskerLeft H α.inv).app (right a✝)
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).f x✝ =
    (𝟙 X).f x✝

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 X).φ i✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).f x✝ =
    (𝟙 X).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : X.I
⊢ ({ f := ⇑e, φ := fun i ↦ (h i).hom } ≫ { f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 X).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).f x✝ =
    (𝟙 Y).f x✝

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 Y).φ i✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
x✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).f x✝ =
    (𝟙 Y).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
e : X.I ≃ Y.I
h : (i : X.I) → X.obj i ≅ Y.obj (e i)
i✝ : Y.I
⊢ ({ f := ⇑e.symm, φ := fun i ↦ eqToHom ⋯ ≫ (h (e.symm i)).inv } ≫ { f := ⇑e, φ := fun i ↦ (h i).hom }).φ i✝ ≫
      eqToHom ⋯ =
    (𝟙 Y).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
x✝ : ((incl C).obj X).I
⊢ (fromIncl (asSigma f).fst (asSigma f).snd).f x✝ = f.f x✝

pp: case h₂
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
i✝ : ((incl C).obj X).I
⊢ (fromIncl (asSigma f).fst (asSigma f).snd).φ i✝ ≫ eqToHom ⋯ = f.φ i✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
x✝ : ((incl C).obj X).I
⊢ (fromIncl (asSigma f).fst (asSigma f).snd).f x✝ = f.f x✝

case h₂
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : FormalCoproduct C
f : (incl C).obj X ⟶ Y
i✝ : ((incl C).obj X).I
⊢ (fromIncl (asSigma f).fst (asSigma f).snd).φ i✝ ≫ eqToHom ⋯ = f.φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝¹ : 𝒜
x✝ : (f x✝¹).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
          x✝¹).f
      x✝ =
    (p x✝¹).f x✝

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝ : 𝒜
i✝ : (f x✝).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
            x✝).φ
        i✝ ≫
      eqToHom ⋯ =
    (p x✝).φ i✝

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝¹ : 𝒜
x✝ : (f x✝¹).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
          x✝¹).f
      x✝ =
    (p x✝¹).f x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
x✝ : 𝒜
i✝ : (f x✝).I
⊢ ((fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p)
            x✝).φ
        i✝ ≫
      eqToHom ⋯ =
    (p x✝).φ i✝
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        none) =
    none

pp: case some
C : Type u
inst✝ : Category.{v, u} C
val✝ : C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        (some val✝)) =
    some val✝

Tactic:
<;>

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        none) =
    none

case some
C : Type u
inst✝ : Category.{v, u} C
val✝ : C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        (some val✝)) =
    some val✝
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        (of a✝)) =
    of a✝

pp: case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        star) =
    star

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        (of a✝)) =
    of a✝

case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        star) =
    star
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
⊢ IsLimit (pullbackCone f g pb)

Tactic:
refine PullbackCone.IsLimit.mk
    (fst := (pullbackCone f g pb).fst) (snd := (pullbackCone f g pb).snd) _
    (fun s ↦ (homPullbackEquiv f g pb hpb s.pt).2 ⟨(s.fst, s.snd), s.condition⟩)
    (fun s ↦ congrArg (·.1.fst)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s ↦ congrArg (·.1.snd)
      ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
    (fun s m h₁ h₂ ↦ ?_)
  convert! ((homPullbackEquiv f g pb hpb s.pt).left_inv m).symm using 3
  rw [← h₁, ← h₂]; rfl

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

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : F.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inl val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inl val✝)

pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : G.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inr val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : F.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inl val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inl val✝)

case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : G.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inr val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : F.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inl val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inl val✝)

pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : G.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inr val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : F.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inl val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inl val✝)

case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : G.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inr val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₁.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inl val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inl val✝)

pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₂.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inr val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₁.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inl val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inl val✝)

case inr
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₂.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inr val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case w
C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

pp: case hf₁
C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ 𝟙 X ≫ f = f

Tactic:
<;>

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

case hf₁
C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ 𝟙 X ≫ f = f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ ≫ h.p₁₂ = φ' ≫ h.p₁₂

pp: case h₁
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ ≫ h.p₂₃ = φ' ≫ h.p₂₃

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ ≫ h.p₁₂ = φ' ≫ h.p₁₂

case h₁
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ ≫ h.p₂₃ = φ' ≫ h.p₂₃
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: case e'_9
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
e_4✝ : X = (pair X Y).obj { as := WalkingPair.left }
⊢ 0 = HasZeroObject.zeroIsTerminal.from ((pair X Y).obj { as := WalkingPair.left })

pp: case e'_10
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
e_5✝ : Y = (pair X Y).obj { as := WalkingPair.right }
⊢ 0 = HasZeroObject.zeroIsTerminal.from ((pair X Y).obj { as := WalkingPair.right })

Tactic:
<;>

Goal state after:
case e'_9
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
e_4✝ : X = (pair X Y).obj { as := WalkingPair.left }
⊢ 0 = HasZeroObject.zeroIsTerminal.from ((pair X Y).obj { as := WalkingPair.left })

case e'_10
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
e_5✝ : Y = (pair X Y).obj { as := WalkingPair.right }
⊢ 0 = HasZeroObject.zeroIsTerminal.from ((pair X Y).obj { as := WalkingPair.right })