mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom
⊢ F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom
⊢ F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A✝ A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
A : Algebra F
h : Limits.IsInitial A
⊢ (F.map (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ F.map A.str) ≫ A.str =
    (F.map (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ { a := F.obj A.a, str := F.map A.str }.str) ≫ A.str

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ⟶ G
X✝ Y✝ : Coalgebra F
f : X✝ ⟶ Y✝
⊢ f.f ≫ Y✝.str ≫ α.app { V := Y✝.V, str := Y✝.str ≫ α.app Y✝.V }.V = f.f ≫ { V := Y✝.V, str := Y✝.str ≫ α.app Y✝.V }.str

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ F.map A.str ≫ F.map (h.from { V := F.obj A.V, str := F.map A.str }).f =
    A.str ≫ { V := F.obj A.V, str := F.map A.str }.str ≫ F.map (h.from { V := F.obj A.V, str := F.map A.str }).f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ F.map (A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f) = F.map (𝟙 A.V)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ F.map (A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f) = F.map (𝟙 A.V)
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (adj.homEquiv A₁.a A₂.a) (A₁.str ≫ f.f) = (adj.homEquiv A₁.a A₂.a) (A₁.str ≫ f.f)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ (adj.homEquiv V₁.V V₂.V).symm (f.f ≫ V₂.str) = (adj.homEquiv V₁.V V₂.V).symm (f.f ≫ V₂.str)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (e₁.inv ⊗ₘ (ε' L W ε).inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom =
    (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫ L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom) =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫ L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom) =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X✝ : Type w
φ✝ : X✝ → X✝ → Prop
X : Type w
φ : X → X → Prop
hφ : IsTrans X φ
x✝ : (Types.pullbackCone (p₂OfRel φ) (p₁OfRel φ)).pt
x₁ snd✝ : X
h : Function.uncurry φ (x₁, snd✝)
fst✝ x₂' : X
h' : Function.uncurry φ (snd✝, x₂')
h₁₂ : snd✝ = fst✝
⊢ ROfRel φ

Tactic:
]

Goal state after:
X✝ : Type w
φ✝ : X✝ → X✝ → Prop
X : Type w
φ : X → X → Prop
hφ : IsTrans X φ
x✝ : (Types.pullbackCone (p₂OfRel φ) (p₁OfRel φ)).pt
x₁ snd✝ : X
h : Function.uncurry φ (x₁, snd✝)
fst✝ x₂' : X
h' : Function.uncurry φ (snd✝, x₂')
h₁₂ : snd✝ = fst✝
⊢ ROfRel φ
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (β_ ((Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ⊗ Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
            (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
        (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁
            (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
          (α_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
                (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³)).inv ≫
            (comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ▷
                Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ≫
              comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
      (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁ comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ≫
        (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)

Tactic:
]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (β_ ((Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ⊗ Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
            (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
        (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁
            (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
          (α_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
                (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³)).inv ≫
            (comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ▷
                Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ≫
              comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
      (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁ comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ≫
        (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (p.map (𝟙 a)) (𝟙 a)

Tactic:
]

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (p.map (𝟙 a)) (𝟙 a)
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ z ⟶[V] y
g : w ⟶ y ⟶[V] x
⊢ (f ⊗ₘ g) ≫
      (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom ≫
        eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
    (β_ v w).hom ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Tactic:
]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ z ⟶[V] y
g : w ⟶ y ⟶[V] x
⊢ (f ⊗ₘ g) ≫
      (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom ≫
        eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
    (β_ v w).hom ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : ForgetEnrichment V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ (((λ_ (𝟙_ V)).inv ≫ (homTo V g ⊗ₘ homTo V f)) ≫
        eComp V (Opposite.unop («to» V z)) (Opposite.unop («to» V y)) (Opposite.unop («to» V x))).op =
    f.op ≫ g.op

Tactic:
]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : ForgetEnrichment V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ (((λ_ (𝟙_ V)).inv ≫ (homTo V g ⊗ₘ homTo V f)) ≫
        eComp V (Opposite.unop («to» V z)) (Opposite.unop («to» V y)) (Opposite.unop («to» V x))).op =
    f.op ≫ g.op
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ (λ_ (𝟙_ V)).inv ≫
      (β_ (𝟙_ V) (𝟙_ V)).hom ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop

Tactic:
]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ (λ_ (𝟙_ V)).inv ≫
      (β_ (𝟙_ V) (𝟙_ V)).hom ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this✝ : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  (β_ (𝟙_ V) (𝟙_ V)).hom ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ ((λ_ (𝟙_ V)).inv ≫ (homTo V f.unop ⊗ₘ homTo V g.unop)) ≫ eComp V x y z = f.unop ≫ g.unop

Tactic:
]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this✝ : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  (β_ (𝟙_ V) (𝟙_ V)).hom ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ ((λ_ (𝟙_ V)).inv ≫ (homTo V f.unop ⊗ₘ homTo V g.unop)) ≫ eComp V x y z = f.unop ≫ g.unop
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ CommSq (p.map φ ≫ p.map ψ) (eqToHom ?ha) (eqToHom ?hb) (f ≫ g)

Tactic:
]

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ CommSq (p.map φ ≫ p.map ψ) (eqToHom ?ha) (eqToHom ?hb) (f ≫ g)
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ T = T

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ S = S

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsCartesian f φ
a' : 𝒳
ψ ψ' : a' ⟶ a
inst✝¹ : p.IsHomLift (𝟙 R) ψ
inst✝ : p.IsHomLift (𝟙 R) ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ IsCartesian.map p f φ (ψ ≫ φ) = IsCartesian.map p f φ (ψ ≫ φ)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
τ : c ⟶ a
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ ≫ φ'.hom = ψ
⊢ (τ ≫ φ) ≫ φ'.hom = ψ

Tactic:
]

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
τ : c ⟶ a
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ ≫ φ'.hom = ψ
⊢ (τ ≫ φ) ≫ φ'.hom = ψ
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
τ : c ⟶ a'
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ'.hom ≫ φ = ψ
⊢ τ ≫ φ'.hom = IsCartesian.map p f φ ψ

Tactic:
]

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
τ : c ⟶ a'
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ'.hom ≫ φ = ψ
⊢ τ ≫ φ'.hom = IsCartesian.map p f φ ψ
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
ψ ψ' : a' ⟶ a
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ map p f φ ⋯ (ψ ≫ φ) = map p f φ ⋯ (ψ ≫ φ)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ f'' = g' ≫ f'

Tactic:
]

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ f'' = g' ≫ f'
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
𝒵 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
⊢ 𝒳.p = 𝒳.p

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ τ = τ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ 𝒳.p.obj a = 𝒳.p.obj a

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
]

Goal state after:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒴.p.IsHomLift f (F.map φ)
⊢ 𝒳.p.IsHomLift f φ

Tactic:
apply of_fac 𝒳.p f φ (F.w_obj a ▸ domain_eq 𝒴.p f (F.map φ))
    (F.w_obj b ▸ codomain_eq 𝒴.p f (F.map φ))

Goal state after:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒴.p.IsHomLift f (F.map φ)
⊢ f = eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
⊢ ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (F₃.obj i)) ≫
      ((diagram V F₁ F₃).obj (Opposite.op i)).map f =
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)) ≫
      ((diagram V F₁ F₃).map f.op).app j

Tactic:
dsimp
    trans (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ _).inv ▷ _ ≫ (_ ◁ (eHomEquiv V (F₂.map f))) ▷ _ ≫ eComp V _ (F₂.obj i) _ ▷ _ ≫
        eComp V _ (F₂.obj j) _
    · have := end_.condition (diagram V F₂ F₃) f
      dsimp [eHomWhiskerLeft, eHomWhiskerRight] at this ⊢
      conv_lhs => rw [assoc, tensorHom_def_assoc]
      conv_rhs =>
        rw [tensorHom_def_assoc, whisker_assoc_assoc, e_assoc,
          triangle_assoc_comp_right_inv_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          assoc, assoc, ← this, MonoidalCategory.whiskerLeft_comp_assoc,
          MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
          ← e_assoc, whiskerLeft_rightUnitor_inv_assoc, associator_inv_naturality_right_assoc,
          Iso.hom_inv_id_assoc, whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc,
          Iso.inv_hom_id_assoc]
    · have := end_.condition (diagram V F₁ F₂) f
      dsimp [eHomWhiskerLeft, eHomWhiskerRight] at this ⊢
      conv_lhs =>
        rw [tensorHom_def'_assoc, ← comp_whiskerRight_assoc,
          ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc,
          assoc, assoc, this, comp_whiskerRight_assoc, comp_whiskerRight_assoc,
          comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc,
          ← associator_inv_naturality_left_assoc, ← e_assoc',
          Iso.inv_hom_id_assoc, ← whisker_exchange_assoc, id_whiskerLeft_assoc,
          Iso.inv_hom_id_assoc]
      conv_rhs => rw [assoc, tensorHom_def'_assoc]

Goal state after: