mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
        F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
by
  rw [← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom, Iso.hom_inv_id]
  simp [mapComp'₀₂₃_hom _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ F.isoMapOfCommSq ⋯ = F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm

Tactic:
ext

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (F.isoMapOfCommSq ⋯).hom =
    (F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ F.isoMapOfCommSq ⋯ = F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm

Tactic:
ext

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ (F.isoMapOfCommSq ⋯).hom =
    (F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
⊢ τ₀' =
    let k := s'.extension;
    let θ := s'.unit;
    let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
    let τ := H.desc sτ;
    let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
    let σ := H'.desc sσ;
    homMk σ ⋯

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := ⋯
H' : (LeftLift.mk h η').IsAbsKan := ⋯
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := ⋯
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
⊢ StructuredArrow.Hom.right τ₀' =
    StructuredArrow.Hom.right
      (let k := s'.extension;
      let θ := s'.unit;
      let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
      let τ := H.desc sτ;
      let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
      let σ := H'.desc sσ;
      homMk σ ⋯)
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝

Tactic:
ext

Goal state after:
case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (𝟙 X✝ ≫ f✝) x✝ = f✝ x✝
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝

Tactic:
ext

Goal state after:
case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (f✝ ≫ 𝟙 Y✝) x✝ = f✝ x✝
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝

Tactic:
ext

Goal state after:
case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
x✝ : W✝
⊢ ((f✝ ≫ g✝) ≫ h✝) x✝ = (f✝ ≫ g✝ ≫ h✝) x✝
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X : Pointed
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X ≃ ((𝟭 Pointed).obj X).X

Tactic:
exact Equiv.optionSubtypeNe X.point

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a ↔ b ∈ f.fix a'

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a → b ∈ f.fix a'

case mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a' → b ∈ f.fix a
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : graphFunctor.map a₁✝ = graphFunctor.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

Goal state after:
X Y Z : RelCat
X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : graphFunctor.map a₁✝ = graphFunctor.map a₂✝
x✝ : X✝
⊢ (ConcreteCategory.hom a₁✝).toFun x✝ = (ConcreteCategory.hom a₂✝).toFun x✝
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y : RelCat
r : X ⟶ Y
⊢ IsIso r ↔ ∃ f, graphFunctor.map f.hom = r

Tactic:
constructor

Goal state after:
case mp
X Y : RelCat
r : X ⟶ Y
⊢ IsIso r → ∃ f, graphFunctor.map f.hom = r

case mpr
X Y : RelCat
r : X ⟶ Y
⊢ (∃ f, graphFunctor.map f.hom = r) → IsIso r
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
⊢ f.preimage Set.univ = f.Dom

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β
x✝ : α
⊢ x✝ ∈ f.preimage Set.univ ↔ x✝ ∈ f.Dom
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f).preimage s = f ⁻¹' s

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x✝ : α
⊢ x✝ ∈ (↑f).preimage s ↔ x✝ ∈ f ⁻¹' s
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
⊢ (f.comp g).Dom = g.preimage f.Dom

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ x✝ ∈ (f.comp g).Dom ↔ x✝ ∈ g.preimage f.Dom
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾f ≫ ↾g = 𝟙 X ∧ ↾g ≫ ↾f = 𝟙 Y

Tactic:
constructor

Goal state after:
case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾f ≫ ↾g = 𝟙 X

case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾g ≫ ↾f = 𝟙 Y
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
⊢ a.bind (f.comp g) = (a.bind g).bind f

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
a✝ : γ
⊢ a✝ ∈ a.bind (f.comp g) ↔ a✝ ∈ (a.bind g).bind f
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
h : (hom (limit.π (F ⋙ objects) x✝¹)) X ⟶ (hom (limit.π (F ⋙ objects) x✝¹)) Y
⊢ (hom (↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map (f ≫ g)).toFunctor.map g_1 ≫ eqToHom ⋯)).toFun h =
    (hom
          ((↾fun g ↦ eqToHom ⋯ ≫ (F.map f).toFunctor.map g ≫ eqToHom ⋯) ≫
            ↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map g).toFunctor.map g_1 ≫ eqToHom ⋯)).toFun
      h

Tactic:
let : Category (objects.obj (F.obj Z)) := (inferInstance : Category (F.obj Z))

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
h : (hom (limit.π (F ⋙ objects) x✝¹)) X ⟶ (hom (limit.π (F ⋙ objects) x✝¹)) Y
this : Category.{v, v} (objects.obj (F.obj Z)) := inferInstance
⊢ (hom (↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map (f ≫ g)).toFunctor.map g_1 ≫ eqToHom ⋯)).toFun h =
    (hom
          ((↾fun g ↦ eqToHom ⋯ ≫ (F.map f).toFunctor.map g ≫ eqToHom ⋯) ≫
            ↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map g).toFunctor.map g_1 ≫ eqToHom ⋯)).toFun
      h
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ ε = toUnit A

Tactic:
ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ = lift (𝟙 A) (𝟙 A)

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ fst A A = lift (𝟙 A) (𝟙 A) ≫ fst A A

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ snd A A = lift (𝟙 A) (𝟙 A) ≫ snd A A
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ F₁ = F₂

Tactic:
apply Functor.curry_obj_injective
  apply Construction.uniq
  apply Functor.flip_injective
  apply Construction.uniq
  apply Functor.flip_injective
  apply Functor.uncurry_obj_injective
  simpa only [Functor.uncurry_obj_curry_obj_flip_flip] using h

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Widesubcategory

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : SymmetricCategory C
inst✝ : P.IsStableUnderBraiding
c c' : WideSubcategory P
⊢ (β_ c c').hom ≫ (β_ c' c).hom = 𝟙 (c ⊗ c')

Tactic:
ext

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : SymmetricCategory C
inst✝ : P.IsStableUnderBraiding
c c' : WideSubcategory P
⊢ ((β_ c c').hom ≫ (β_ c' c).hom).hom = (𝟙 (c ⊗ c')).hom
Module: Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : P.IsStableUnderBraiding
c : WideSubcategory P
inst✝² : ComonObj c.obj
inst✝¹ : IsCommComonObj c.obj
inst✝ : P.IsStableUnderComonoid c.obj
⊢ Δ ≫ (β_ c c).hom = Δ

Tactic:
ext

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : P.IsStableUnderBraiding
c : WideSubcategory P
inst✝² : ComonObj c.obj
inst✝¹ : IsCommComonObj c.obj
inst✝ : P.IsStableUnderComonoid c.obj
⊢ (Δ ≫ (β_ c c).hom).hom = Δ.hom
Module: Mathlib.CategoryTheory.Dialectica.Basic

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

Tactic:
ext

Goal state after:
case e_a.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ 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
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: case e_self
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext

Goal state after:
case e_self.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ 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 Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝² : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst✝¹ : ChosenPullbacksAlong g'
inst✝ : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_3
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_5
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_7
⊢ g'' ≫ δ₃ ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g

Tactic:
rw [reassoc_of% comm₂', comm₂, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: 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₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
ext

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
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:
ext

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.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ coprod.inl ≫ coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr) = X ◁ coprod.inl

Tactic:
coprod.inl_desc

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ X ◁ coprod.inl = X ◁ coprod.inl
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ≫ coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X) = coprod.inl ▷ X

Tactic:
coprod.inl_desc

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ▷ X = coprod.inl ▷ X
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: 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
⊢ ∂R X Y Z = coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)

Tactic:
ext

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.Distributive.Monoidal

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

Tactic:
ext

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: 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 = (λ_ X).hom ≫ f

Tactic:
ext

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 hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F) =
    π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), prod.map π₂ (𝟙 Y.tgt) ≫ f.F)

Tactic:
ext

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

Goal state before:
pp: case h₂.e_a
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:
ext

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: 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 = (ρ_ X).hom ≫ f

Tactic:
ext

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
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) =
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt))

Tactic:
ext

Goal state after:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) ≫ π₁ =
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) ≫ π₁
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hF.h₁.e_a
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:
ext

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.Dialectica.Monoidal

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

Tactic:
ext

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

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