mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
⊢ φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x ≫ G'.map (α.right.app x)) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)

Tactic:
Functor.map_comp_assoc

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
⊢ φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      φ.base.map (G'.map (α.right.app x)) ≫ (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasWeakPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasWeakPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ (fst f₁ f₂ ≫ i₁) ≫ g₁ = (snd f₁ f₂ ≫ i₂) ≫ g₂

Tactic:
by simp only [Category.assoc, ← eq₁, ← eq₂, weakPullback.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ (weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.fst) ≫ f =
    (weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd) ≫ g

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.fst ≫ f =
    (weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd) ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
⊢ G.map f.snd = (x.iso.inv ≫ F.map f.fst) ≫ y.iso.hom

Tactic:
Category.assoc,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
⊢ G.map f.snd = x.iso.inv ≫ F.map f.fst ≫ y.iso.hom
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂)) ≫
      F.map (e₁.hom ▷ L.obj X₂) =
    (((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
        F.map (Y₁ ◁ e₂.hom)) ≫
      F.map (e₁.hom ▷ L.obj X₂)

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) ≫ F.map (e₁.hom ▷ L.obj X₂) =
    (((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
        F.map (Y₁ ◁ e₂.hom)) ≫
      F.map (e₁.hom ▷ L.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
        F.map (Y₁ ◁ e₂.hom)) ≫
      F.map (e₁.hom ▷ L.obj X₂)

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    ((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
        μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
      F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    ((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
        μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
      F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      (μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
        F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      (μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
        F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        ((Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
          F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        ((Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))) ≫
          F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map ((δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ (e₁.hom ⊗ₘ e₂.hom))

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv) ≫ (e₁.hom ⊗ₘ e₂.hom))
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ (curry (β_ I A).hom ≫ (ihom I).map (Hom.left u)) ≫ (ihom I).map X.hom = toUnit A ≫ curryRightUnitorHom I

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry (β_ I A).hom ≫ (ihom I).map (Hom.left u) ≫ (ihom I).map X.hom = toUnit A ≫ curryRightUnitorHom I
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
comm : toUnit A ≫ curry (ρ_ I).hom = v₂ ≫ (ihom I).map X.hom
w' : I ◁ toUnit A ≫ (ρ_ I).hom = ((ihom.adjunction I).homEquiv A X.left).symm v₂ ≫ X.hom
⊢ ((β_ A I).hom ≫ ((ihom.adjunction I).homEquiv A X.left).symm v₂) ≫ X.hom = SemiCartesianMonoidalCategory.snd A I

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
comm : toUnit A ≫ curry (ρ_ I).hom = v₂ ≫ (ihom I).map X.hom
w' : I ◁ toUnit A ≫ (ρ_ I).hom = ((ihom.adjunction I).homEquiv A X.left).symm v₂ ≫ X.hom
⊢ (β_ A I).hom ≫ ((ihom.adjunction I).homEquiv A X.left).symm v₂ ≫ X.hom = SemiCartesianMonoidalCategory.snd A I
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
⊢ 𝟭 (KleisliCat m) ≅
    { obj := fun X ↦ { of := X }, map := fun {X Y} f ↦ { of := ↾f }, map_id := ⋯, map_comp := ⋯ } ⋙
      { obj := fun X ↦ X.of, map := fun {X Y} f x ↦ (ConcreteCategory.hom f.of) x, map_id := ⋯, map_comp := ⋯ }

Tactic:
refine NatIso.ofComponents (fun X => Iso.refl X) fun f => ?_

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f : X✝ ⟶ Y✝
⊢ (𝟭 (KleisliCat m)).map f ≫ (Iso.refl Y✝).hom =
    (Iso.refl X✝).hom ≫
      ({ obj := fun X ↦ { of := X }, map := fun {X Y} f ↦ { of := ↾f }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun X ↦ X.of, map := fun {X Y} f x ↦ (ConcreteCategory.hom f.of) x, map_id := ⋯,
              map_comp := ⋯ }).map
        f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔
    G.map ((F.map (adj.unit.app A.A) ≫ F.map (G.map f)) ≫ adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔
    G.map (F.map (adj.unit.app A.A) ≫ F.map (G.map f) ≫ adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f