mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
g : (Sum.inl_ C C').obj x✝ ⟶ (Sum.inl_ C C').obj y✝
⊢ (Sum.inl_ C C').map f✝ = g

pp: case inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝ : x✝ ⟶ y✝
g : (Sum.inr_ C C').obj x✝ ⟶ (Sum.inr_ C C').obj y✝
⊢ (Sum.inr_ C C').map f✝ = g

Tactic:
<;>

Goal state after:
case inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
g : (Sum.inl_ C C').obj x✝ ⟶ (Sum.inl_ C C').obj y✝
⊢ (Sum.inl_ C C').map f✝ = g

case inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝ : x✝ ⟶ y✝
g : (Sum.inr_ C C').obj x✝ ⟶ (Sum.inr_ C C').obj y✝
⊢ (Sum.inr_ C C').map f✝ = g
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case e'_4
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
<;>

Goal state after:
case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case e'_4
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)).f = (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂).f

pp: case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)).F = (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂).F

Tactic:
<;>

Goal state after:
case hf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)).f = (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂).f

case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)).F = (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂).F
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) ≫ π₁ =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
        prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) ≫
      π₁

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) ≫ π₂ =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
        prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) ≫
      π₂

Tactic:
<;>

Goal state after:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) ≫ π₁ =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
        prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) ≫
      π₁

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) ≫ π₂ =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
        prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) ≫
      π₂
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F = prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F = prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F

Tactic:
<;>

Goal state after:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F = prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F = prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: 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 ⥤ C
G : B ⥤ C
val✝ : A
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inl val✝)) =
    𝟙
      (match inl val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)

pp: 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 ⥤ C
G : B ⥤ C
val✝ : B
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inr val✝)) =
    𝟙
      (match inr val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)

Tactic:
<;>

Goal state after:
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 ⥤ C
G : B ⥤ C
val✝ : A
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inl val✝)) =
    𝟙
      (match inl val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)

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 ⥤ C
G : B ⥤ C
val✝ : B
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inr val✝)) =
    𝟙
      (match inr val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: 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 ⥤ C
G : B ⥤ C
z : A ⊕ B
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
g : (Sum.inl_ A B).obj y✝ ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝ ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

pp: 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 ⥤ C
G : B ⥤ C
z : A ⊕ B
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
g : (Sum.inr_ A B).obj y✝ ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝ ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

Tactic:
<;>

Goal state after:
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 ⥤ C
G : B ⥤ C
z : A ⊕ B
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
g : (Sum.inl_ A B).obj y✝ ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝ ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

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 ⥤ C
G : B ⥤ C
z : A ⊕ B
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
g : (Sum.inr_ A B).obj y✝ ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝ ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: case h₁
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂R X Y Z).hom = coprod.inl ≫ (coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)).hom

pp: case h₂
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ≫ (coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)).hom

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂R X Y Z).hom = coprod.inl ≫ (coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)).hom

case h₂
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ≫ (coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)).hom
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inl.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 ⥤ C
G : B ⥤ C
x✝ y✝¹ : A
f✝¹ : x✝ ⟶ y✝¹
y✝ : A
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹ ≫ (Sum.inl_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝)

pp: case inr.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 ⥤ C
G : B ⥤ C
x✝ y✝¹ : B
f✝¹ : x✝ ⟶ y✝¹
y✝ : B
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹ ≫ (Sum.inr_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝)

Tactic:
<;>

Goal state after:
case inl.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 ⥤ C
G : B ⥤ C
x✝ y✝¹ : A
f✝¹ : x✝ ⟶ y✝¹
y✝ : A
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹ ≫ (Sum.inl_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝)

case inr.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 ⥤ C
G : B ⥤ C
x✝ y✝¹ : B
f✝¹ : x✝ ⟶ y✝¹
y✝ : B
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹ ≫ (Sum.inr_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝)
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: case h₁
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ coprod.inl ≫ curry (∂L X Y Z).inv = coprod.inl ≫ coprod.desc (curry coprod.inl) (curry coprod.inr)

pp: case h₂
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ coprod.inr ≫ curry (∂L X Y Z).inv = coprod.inr ≫ coprod.desc (curry coprod.inl) (curry coprod.inr)

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ coprod.inl ≫ curry (∂L X Y Z).inv = coprod.inl ≫ coprod.desc (curry coprod.inl) (curry coprod.inr)

case h₂
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ coprod.inr ≫ curry (∂L X Y Z).inv = coprod.inr ≫ coprod.desc (curry coprod.inl) (curry coprod.inr)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((𝟙 (𝟙_ (Dial C)) ⊗ₘ f) ≫ (λ_ Y).hom).f = ((λ_ X).hom ≫ f).f

pp: case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((𝟙 (𝟙_ (Dial C)) ⊗ₘ f) ≫ (λ_ Y).hom).F = ((λ_ X).hom ≫ f).F

Tactic:
<;>

Goal state after:
case hf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((𝟙 (𝟙_ (Dial C)) ⊗ₘ f) ≫ (λ_ Y).hom).f = ((λ_ X).hom ≫ f).f

case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((𝟙 (𝟙_ (Dial C)) ⊗ₘ f) ≫ (λ_ Y).hom).F = ((λ_ X).hom ≫ f).F
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₂.e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) ≫ π₁ = prod.map π₂ (𝟙 Y.tgt) ≫ π₁

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) ≫ π₂ = prod.map π₂ (𝟙 Y.tgt) ≫ π₂

Tactic:
<;>

Goal state after:
case h₂.e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) ≫ π₁ = prod.map π₂ (𝟙 Y.tgt) ≫ π₁

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) ≫ π₂ = prod.map π₂ (𝟙 Y.tgt) ≫ π₂
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((f ⊗ₘ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom).f = ((ρ_ X).hom ≫ f).f

pp: case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((f ⊗ₘ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom).F = ((ρ_ X).hom ≫ f).F

Tactic:
<;>

Goal state after:
case hf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((f ⊗ₘ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom).f = ((ρ_ X).hom ≫ f).f

case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ ((f ⊗ₘ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom).F = ((ρ_ X).hom ≫ f).F
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hF.h₁.e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) ≫ π₁ = prod.map π₁ (𝟙 Y.tgt) ≫ π₁

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) ≫ π₂ = prod.map π₁ (𝟙 Y.tgt) ≫ π₂

Tactic:
<;>

Goal state after:
case hF.h₁.e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) ≫ π₁ = prod.map π₁ (𝟙 Y.tgt) ≫ π₁

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) ≫ π₂ = prod.map π₁ (𝟙 Y.tgt) ≫ π₂
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a : α
⊢ pullback.fst g₁ (Sigma.ι X a) ≫ g₁ ≫ Sigma.desc e = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e

Tactic:
rw [← Category.assoc, pullback.condition]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a : α
⊢ (pullback.snd g₁ (Sigma.ι X a) ≫ Sigma.ι X a) ≫ Sigma.desc e = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: 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 G : A ⥤ C
H I : B ⥤ C
α : F ⟶ G
β : H ⟶ I
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
⊢ ((F.sum' H).map ((Sum.inl_ A B).map f✝) ≫
      match (Sum.inl_ A B).obj y✝ with
      | inl X => α.app X
      | inr X => β.app X) =
    (match (Sum.inl_ A B).obj x✝ with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map ((Sum.inl_ A B).map f✝)

pp: 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 G : A ⥤ C
H I : B ⥤ C
α : F ⟶ G
β : H ⟶ I
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
⊢ ((F.sum' H).map ((Sum.inr_ A B).map f✝) ≫
      match (Sum.inr_ A B).obj y✝ with
      | inl X => α.app X
      | inr X => β.app X) =
    (match (Sum.inr_ A B).obj x✝ with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map ((Sum.inr_ A B).map f✝)

Tactic:
<;>

Goal state after:
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 G : A ⥤ C
H I : B ⥤ C
α : F ⟶ G
β : H ⟶ I
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
⊢ ((F.sum' H).map ((Sum.inl_ A B).map f✝) ≫
      match (Sum.inl_ A B).obj y✝ with
      | inl X => α.app X
      | inr X => β.app X) =
    (match (Sum.inl_ A B).obj x✝ with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map ((Sum.inl_ A B).map f✝)

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 G : A ⥤ C
H I : B ⥤ C
α : F ⟶ G
β : H ⟶ I
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
⊢ ((F.sum' H).map ((Sum.inr_ A B).map f✝) ≫
      match (Sum.inr_ A B).obj y✝ with
      | inl X => α.app X
      | inr X => β.app X) =
    (match (Sum.inr_ A B).obj x✝ with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map ((Sum.inr_ A B).map f✝)