mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ ((α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ ((α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ ((β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ ((β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ ((α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ ((α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (𝟙 x)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (𝟙 x)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).ContainsIdentities
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).ContainsIdentities

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).ContainsIdentities
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).ContainsIdentities
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : Set (MorphismProperty C)
h : ∀ W' ∈ W, W'.IsStableUnderComposition
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : ∀ W_1 ∈ W, W_1 f
hg : ∀ W_1 ∈ W, W_1 g
⊢ ∀ W_1 ∈ W, W_1 (f ≫ g)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : Set (MorphismProperty C)
h : ∀ W' ∈ W, W'.IsStableUnderComposition
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : ∀ W_1 ∈ W, W_1 f
hg : ∀ W_1 ∈ W, W_1 g
⊢ ∀ W_1 ∈ W, W_1 (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsStableUnderComposition
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).IsStableUnderComposition

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsStableUnderComposition
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).IsStableUnderComposition
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : F₁.map f ≫ app Y✝ = app X✝ ≫ F₂.map f
hg : F₁.map g ≫ app Z✝ = app Y✝ ≫ F₂.map g
⊢ app X✝ ≫ F₂.map f ≫ F₂.map g = app X✝ ≫ F₂.map f ≫ F₂.map g

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X = F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom =
    ((α_ X Y Z).inv ≫
        𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)) ≫
      (α_ Z Y X).hom

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom =
    ((α_ X Y Z).inv ≫
        𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)) ≫
      (α_ Z Y X).hom
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : IsIso f
hg : IsIso g
⊢ IsIso (f ≫ g)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : IsIso f
hg : IsIso g
⊢ IsIso (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : Mono f
hg : Mono g
⊢ Mono (f ≫ g)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : Mono f
hg : Mono g
⊢ Mono (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsMultiplicative
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).IsMultiplicative

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsMultiplicative
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).IsMultiplicative
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g : Y✝ ⟶ Z✝
x✝ : C
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure f

Tactic:
]

Goal state after:
case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g : Y✝ ⟶ Z✝
x✝ : C
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure f
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g✝ : Y✝ ⟶ Z✝
x✝ y✝ z✝ : C
f' : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X✝ ⟶ x✝), W.multiplicativeClosure f → W.multiplicativeClosure (f ≫ f')
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure ((f ≫ f') ≫ g)

Tactic:
]

Goal state after:
case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g✝ : Y✝ ⟶ Z✝
x✝ y✝ z✝ : C
f' : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X✝ ⟶ x✝), W.multiplicativeClosure f → W.multiplicativeClosure (f ≫ f')
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure ((f ≫ f') ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
x✝ : C
g : x✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' g

Tactic:
]

Goal state after:
case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
x✝ : C
g : x✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' g
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case of_comp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
g' : x✝ ⟶ y✝
f : y✝ ⟶ z✝
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z✝ ⟶ Z✝), W.multiplicativeClosure' g → W.multiplicativeClosure' (f ≫ g)
g : z✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (g' ≫ f ≫ g)

Tactic:
]

Goal state after:
case of_comp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
g' : x✝ ⟶ y✝
f : y✝ ⟶ z✝
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z✝ ⟶ Z✝), W.multiplicativeClosure' g → W.multiplicativeClosure' (f ≫ g)
g : z✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (g' ≫ f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.multiplicativeClosure.IsMultiplicative

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.multiplicativeClosure.IsMultiplicative
Module: Mathlib.CategoryTheory.Monoidal.Braided.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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ (β_ (F.obj X✝) (F.obj Y✝)).hom ≫ μ F Y✝ X✝ ≫ F.map (f✝ ▷ X✝) =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ≫ μ F Y✝ X✝ ≫ F.map (f✝ ▷ X✝)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ Injective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ Injective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ Bijective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ Bijective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X = F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝ ≫ F.map (Z✝ ◁ f✝) =
    (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝ ≫ F.map (Z✝ ◁ f✝)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f : Arrow (Type u)
x₁ x₂ :
  (fun X ↦ X)
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
          map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
      f)
h :
  (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₁ =
    (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₂
⊢ ↑x₁ = ↑x₂

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f : Arrow (Type u)
x₁ x₂ :
  (fun X ↦ X)
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
          map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
      f)
h :
  (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₁ =
    (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₂
⊢ ↑x₁ = ↑x₂
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.surjective C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.surjective C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Epi ((forget C).map f)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Epi ((forget C).map f)
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Function.Injective ⇑(hom ((forget C).map f))

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Function.Injective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.injective C f
⊢ Function.Injective ⇑(hom ((forget C).map f))

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.injective C f
⊢ Function.Injective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ Mono ((forget C).map f)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ Mono ((forget C).map f)
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget C).PreservesMonomorphisms

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget C).PreservesMonomorphisms
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesEpimorphisms
⊢ (forget C).PreservesEpimorphisms

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesEpimorphisms
⊢ (forget C).PreservesEpimorphisms