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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
X : C
f : X ⟶ Y
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ inv (η ▷ h) = inv η ▷ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i) =
    inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom) =
    inv ((α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv) =
    inv ((α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
e' : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e' g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) =
    inv ((α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) =
    inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X✝ : C
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e e' : F.CorepresentableBy X
h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
Y : C
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
⊢ (yoneda.obj Y).map f ≫ r.homEquiv.toIso.hom = r.homEquiv.toIso.hom ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
Y : C
e : yoneda.obj Y ≅ F
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (e.app (op X)).toEquiv (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) ((e.app (op X')).toEquiv g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X✝ : C
r : F.CorepresentableBy X✝
X X' : C
f : X ⟶ X'
⊢ (coyoneda.obj (op X✝)).map f ≫ r.homEquiv.toIso.hom = r.homEquiv.toIso.hom ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X✝ : C
e : coyoneda.obj (op X✝) ≅ F
X X' : C
f : X ⟶ X'
g : X✝ ⟶ X
⊢ (e.app X').toEquiv (g ≫ f) = (ConcreteCategory.hom (F.map f)) ((e.app X).toEquiv g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
R : F.RepresentableBy X
e : Y ≅ X
⊢ ∀ {X_1 X' : C} (f : X_1 ⟶ X') (g : X' ⟶ Y),
    (e.homToEquiv.trans R.homEquiv) (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) ((e.homToEquiv.trans R.homEquiv) g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
R : F.CorepresentableBy X
e : Y ≅ X
⊢ ∀ {Y_1 Y' : C} (g : Y_1 ⟶ Y') (f : Y ⟶ Y_1),
    (e.homFromEquiv.trans R.homEquiv) (f ≫ g) = (ConcreteCategory.hom (F.map g)) ((e.homFromEquiv.trans R.homEquiv) f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.RepresentableBy X
⊢ (fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.RepresentableBy Y
⊢ (fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.CorepresentableBy X
⊢ (fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.CorepresentableBy Y
⊢ (fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
X : C
R : F.RepresentableBy X
X✝ X'✝ : C
f : X✝ ⟶ X'✝
g : X'✝ ⟶ X
⊢ (R.homEquiv.trans Equiv.ulift.symm) (f ≫ g) =
    (ConcreteCategory.hom ((F ⋙ uliftFunctor.{w, v}).map f.op)) ((R.homEquiv.trans Equiv.ulift.symm) g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
R : F.CorepresentableBy X
Y✝ Y'✝ : C
f : Y✝ ⟶ Y'✝
g : X ⟶ Y✝
⊢ (R.homEquiv.trans Equiv.ulift.symm) (g ≫ f) =
    (ConcreteCategory.hom ((F ⋙ uliftFunctor.{w, v}).map f)) ((R.homEquiv.trans Equiv.ulift.symm) g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X : C
R : F.RepresentableBy X
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.obj X).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X : C
R : F.CorepresentableBy X
⊢ ∀ {X_1 Y : C} (f : X_1 ⟶ Y),
    (uliftCoyoneda.{w, v₁, u₁}.obj (op X)).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : F.IsRepresentable
X : Cᵒᵖ
f : unop X ⟶ F.reprX
⊢ (ConcreteCategory.hom (F.reprW.hom.app X)) f = (ConcreteCategory.hom (F.map f.op)) F.reprx

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : F.IsCorepresentable
X : C
f : F.coreprX ⟶ X
⊢ (ConcreteCategory.hom (F.coreprW.hom.app X)) f = (ConcreteCategory.hom (F.map f)) F.coreprx

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ inv ((λ_ f).inv ▷ g) = inv ((λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
⊢ Function.LeftInverse
    (fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ }) fun η ↦
    (ConcreteCategory.hom (η.app (op X))) (𝟙 X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
⊢ Function.RightInverse
    (fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ }) fun η ↦
    (ConcreteCategory.hom (η.app (op X))) (𝟙 X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.map g.op)) (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ yonedaEquiv (yoneda.map f) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Cᵒᵖ ⥤ Type v₁
x : F.obj (op X)
⊢ yoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm ((ConcreteCategory.hom (F.map f.op)) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom

Tactic:
←
      associator_inv_naturality_middle,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ f ◁ (ρ_ g).hom ▷ 𝟙 c ≫ (α_ f g (𝟙 c)).inv =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F F' : Cᵒᵖ ⥤ Type v₁
f : F ⟶ F'
x : F.obj (op X)
⊢ yonedaEquiv.symm x ≫ f = yonedaEquiv.symm ((ConcreteCategory.hom (f.app (op X))) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ inv (f ◁ (ρ_ g).inv) = inv ((ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.map g.op)) (yonedaEquiv f) = (ConcreteCategory.hom (f.app (op Y))) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (yonedaEquiv f) = (ConcreteCategory.hom (f.app Y)) g.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
t : F.obj X
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) = yoneda.map f.unop ≫ yonedaEquiv.symm t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)} (f : X ⟶ Y),
    (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom ≫ (evaluation Cᵒᵖ (Type u₁)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ ∀ {X_1 Y : Cᵒᵖ ⥤ Type v₁} (f : X_1 ⟶ Y),
    ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type v₁) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: C : Cat
⊢ ↾Quot.map (𝟙 C).toFunctor.obj ⋯ = 𝟙 (Quotient (isIsomorphicSetoid ↑C))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ ↾Quot.map (f ≫ g).toFunctor.obj ⋯ = ↾Quot.map f.toFunctor.obj ⋯ ≫ ↾Quot.map g.toFunctor.obj ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Thin

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
x✝¹ x✝ : D ⥤ C
α β : x✝¹ ⟶ x✝
⊢ α.app = β.app

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Thin

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
⊢ ∀ (a b : X ≅ Y), a = b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫ yonedaEquiv.toIso.hom =
      yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ (fun x ↦ x ≫ f) (f ≫ g) = (fun x ↦ x ≫ f) (𝟙 X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x ↦ x ≫ f

Tactic:
by

Goal state after: