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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
e : F.obj X ≅ F.obj Y
⊢ F.map (hF.preimage e.inv ≫ hF.preimage e.hom) = F.map (𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
E' : Type u₄
inst✝¹ : Category.{v₄, u₄} E'
F G : C ⥤ D
X✝ Y : C
α : F ⟶ G
inst✝ : IsIso α
X : C
⊢ α.app X ≫ (inv α).app X = 𝟙 (F.obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
E' : Type u₄
inst✝¹ : Category.{v₄, u₄} E'
F G : C ⥤ D
X✝ Y : C
α : F ⟶ G
inst✝ : IsIso α
X : C
⊢ (inv α).app X ≫ α.app X = 𝟙 (G.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : IsIso α
X : C
⊢ (inv α).app X = inv (α.app X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
⊢ Function.LeftInverse hF.preimageIso F.mapIso

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D ⥤ E
X Y : C
e : X ≅ Y
Z : D
⊢ inv ((F.map e.inv).app Z) = (F.map e.hom).app Z

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
⊢ Function.RightInverse hF.preimageIso F.mapIso

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
G : C ⥤ D
e : F ≅ G
X✝ Y✝ : C
f : G.obj X✝ ⟶ G.obj Y✝
⊢ G.map (hF.preimage (e.hom.app X✝ ≫ f ≫ e.inv.app Y✝)) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D
X✝ Y✝ : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
⊢ G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
⊢ Nonempty F.FullyFaithful

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), IsIso (α.app X)
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (asIso (α.app Y)).hom = (asIso (α.app X)).hom ≫ G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
obj : C → D
e : (X : C) → F.obj X ≅ obj X
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ (F.copyObj obj e).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₁✝ = F.map a₂✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ E
inst✝¹ : F.Faithful
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ Faithful.div F G obj h_obj map h_map ⋙ G = F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Full
inst✝ : G.Full
X✝ Y✝ : C
f : (F ⋙ G).obj X✝ ⟶ (F ⋙ G).obj Y✝
⊢ (F ⋙ G).map (F.preimage (G.preimage f)) = f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
⊢ F.Full

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : H.Full
inst✝ : H.Faithful
comp_iso : F ⋙ H ≅ G ⋙ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ H.map (F.map f ≫ (H.preimageIso (comp_iso.app Y✝)).hom) = H.map ((H.preimageIso (comp_iso.app X✝)).hom ≫ G.map f)

Tactic:
by

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

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
X Y : C
f g : X ⟶ Y
h : (fun f ↦ ⇑(hom f)) f = (fun f ↦ ⇑(hom f)) g
⊢ f = g

Tactic:
by

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

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
X : C
⊢ ⇑(hom (𝟙 X)) = id

Tactic:
by

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

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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ⇑(hom (f ≫ g)) = ⇑(hom g) ∘ ⇑(hom f)

Tactic:
by

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

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
X : C
x : ToType X
⊢ (hom (𝟙 X)) x = x

Tactic:
by

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

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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType X
⊢ (hom (f ≫ g)) x = (hom g) ((hom f) x)

Tactic:
by

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

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
X : C
⊢ ⇑(ConcreteCategory.hom (𝟙 X)) = id

Tactic:
by

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

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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ⇑(ConcreteCategory.hom (f ≫ g)) = ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)

Tactic:
by

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

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
C : Type u
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
f : C → D
X✝ Y✝ : InducedCategory D f
x✝ : X✝ ⟶ Y✝
⊢ homMk (ofHom (hom x✝.hom)) = x✝

Tactic:
by

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

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✝
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
P : ObjectProperty C
X✝ Y✝ : P.FullSubcategory
x✝ : X✝ ⟶ Y✝
⊢ homMk (ofHom (hom x✝.hom)) = x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F G : C ⥤ D
φ : F ⟶ G
X Y : C
f : X ⟶ Y
x : ToType (F.obj X)
⊢ (ConcreteCategory.hom (φ.app Y)) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (φ.app X)) x)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ τ (σ X) ⟶ τ (σ Y)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Elementwise

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
x✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : f = g
x : CC X
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).map f) ≍ ⋯ ▸ ⋯ ▸ φ.map f

Tactic:
apply (cast_heq _ _).trans

Goal state after:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ ⋯.mpr (φ.map f) ≍ ⋯ ▸ ⋯ ▸ φ.map f
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ ⋯.mpr (φ.map f) ≍ ⋯ ▸ ⋯ ▸ φ.map f

Tactic:
apply (cast_heq _ _).trans

Goal state after:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ φ.map f ≍ ⋯ ▸ ⋯ ▸ φ.map f
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: a b c : Prop
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: a b c : Prop
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: a b c : Prop
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ of σ ⋙q lift σ φ τ h = φ

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
⊢ (dite p a fun hp ↦ dite q (b hp) (c hp)) = if hq : q then dite p a fun hp ↦ b hp hq else dite p a fun hp ↦ c hp hq

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
e : b ⟶ a
h : nil = p.cons e
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
e : b ⟶ a
h : p.cons e = nil
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X =
    { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.obj X

Tactic:
simp only

Goal state after:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X = τ X
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun hp ↦ dite q (a hp) (b hp)) c = if hq : q then dite p (fun hp ↦ a hp hq) c else dite p (fun hp ↦ b hp hq) c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ b = c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ p ≍ p'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
⊢ f True ∧ f False → ∀ (p : Prop), f p

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ e ≍ e'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
⊢ f True ∨ f False → ∃ p, f p

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
hzero : p.length = 0
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a : V
p : Path a a
hzero : p.length = 0
⊢ p = nil

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a x✝ b✝ : V
p : Path a b✝
a✝ : b✝ ⟶ x✝
⊢ nil.comp (p.cons a✝) = p.cons a✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ = lift σ φ τ h

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.IsoReassoc

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ≅ Y
w : f = g
Z : C
h : Y ≅ Z
⊢ f ≪≫ h = g ≪≫ h

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ (p.comp q).comp (r.cons a✝) = p.comp (q.comp (r.cons a✝))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
by rintro ⟨rfl, rfl⟩; rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
⊢ p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
h_eq : p₁.comp q₁ = p₂.comp q₂
⊢ p₂.length + q₁.length = p₂.length + q₂.length

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
by rintro ⟨rfl, rfl⟩; rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
⊢ reverse (reverse f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ f = reverse g ↔ reverse f = g

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁷ : Quiver U
inst✝⁶ : Quiver V
inst✝⁵ : Quiver W
inst✝⁴ : HasReverse U
inst✝³ : HasReverse V
inst✝² : HasReverse W
φ : U ⥤q V
ψ : V ⥤q W
inst✝¹ : φ.MapReverse
inst✝ : ψ.MapReverse
u✝ v✝ : U
e : u✝ ⟶ v✝
⊢ (φ ⋙q ψ).map (reverse e) = reverse ((φ ⋙q ψ).map e)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝¹ : Quiver V
inst✝ : HasReverse V
a b c : V
p : Path a b
q : Path b c
⊢ (p.comp q).reverse = q.reverse.comp p.reverse

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
p : Path a b
⊢ p.reverse.reverse = p

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
q : c ⟶ d
n✝ : ℕ
x : V
q'' : a ⟶ x
p'' : Path x c
hl : p''.length = n✝
h : ∀ {n : ℕ}, (q''.toPath.comp p'').length = n + 1 → ∃ c_1 f q x_1, q''.toPath.comp p'' = f.toPath.comp q
hp : (q''.toPath.comp p'').length = n✝ + 1
⊢ (p''.cons q).length = n✝ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ of ⋙q lift φ = φ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
n : ℕ
hp : p.length = n + 1
⊢ ∃ c f q x, p = f.toPath.comp q

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1

Tactic:
by

Goal state after: