mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
      zero := ⋯ }.Exact

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ ((opcyclesFunctor C c i).mapShortComplex.obj S).Exact

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Epi ((opcyclesFunctor C c i).mapShortComplex.obj S).g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V₁ : Type u₁
V₂ : Type u₂
V₃ : Type u₃
inst✝² : Quiver V₁
inst✝¹ : Quiver V₂
inst✝ : Quiver V₃
F : V₁ ⥤q V₂
G : V₂ ⥤q V₃
X✝ Y✝ : Paths V₁
f : X✝ ⟶ Y✝
⊢ (freeMap (F ⋙q G)).map f ≫ (Iso.refl ((freeMap (F ⋙q G)).obj Y✝)).hom =
    (Iso.refl ((freeMap (F ⋙q G)).obj X✝)).hom ≫ (freeMap F ⋙ freeMap G).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ X = e.hom.obj (e.inv.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ ((cyclesFunctor C c j).mapShortComplex.obj S).Exact

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ Y = e.hom.obj (e.inv.obj Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS✝ : S.ShortExact
i✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Mono ((cyclesFunctor C c j).mapShortComplex.obj S).f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
f : X ⟶ Y
⊢ X = e.inv.obj (e.hom.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
f : X ⟶ Y
⊢ Y = e.inv.obj (e.hom.obj Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ e.inv.obj (e.hom.obj X) = X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ e.inv.obj (e.hom.obj Y) = Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
f : X ⟶ Y
⊢ (fun g ↦ Quiver.homOfEq (e.inv.map g) ⋯ ⋯) ((fun f ↦ e.hom.map f) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ (fun f ↦ e.hom.map f) ((fun g ↦ Quiver.homOfEq (e.inv.map g) ⋯ ⋯) g) = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (asIso (S.X₁.homologyι i)).hom ≫ (S.map (HomologicalComplex.opcyclesFunctor C c i)).f =
    (S.map (HomologicalComplex.homologyFunctor C c i)).f ≫ (asIso (S.X₂.homologyι i)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (asIso (S.X₂.homologyι i)).hom ≫ (S.map (HomologicalComplex.opcyclesFunctor C c i)).g =
    (S.map (HomologicalComplex.homologyFunctor C c i)).g ≫ (asIso (S.X₃.homologyι i)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ e X = X''

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ e Y = Y''

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ Quiver.homOfEq ((he X' Y') (Quiver.homOfEq f hX hY)) hX' hY' = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of W)
f : X ⟶ Y
⊢ X = e (e.symm X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of W)
f : X ⟶ Y
⊢ Y = e (e.symm Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of V)
f : X ⟶ Y
⊢ e (e.symm (e X)) = e X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of V)
f : X ⟶ Y
⊢ e (e.symm (e Y)) = e Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of V)
f : X ⟶ Y
⊢ ({ obj := ⇑e, map := fun {X Y} ↦ ⇑(he X Y) } ≫
          { obj := ⇑e.symm, map := fun {X Y} f ↦ (he (e.symm X) (e.symm Y)).symm (Quiver.homOfEq f ⋯ ⋯) }).map
      f =
    Quiver.homOfEq ((𝟙 (of V)).map f) ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
⊢ ∀ (X Y : ↑(of W)) (f : X ⟶ Y),
    ({ obj := ⇑e.symm, map := fun {X Y} f ↦ (he (e.symm X) (e.symm Y)).symm (Quiver.homOfEq f ⋯ ⋯) } ≫
            { obj := ⇑e, map := fun {X Y} ↦ ⇑(he X Y) }).map
        f =
      Quiver.homOfEq ((𝟙 (of W)).map f) ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: C : Type u
D : Type u₁
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).map f.toPath ≫
        (Iso.refl ((Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj Y)).hom =
      (Iso.refl ((Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj X)).hom ≫ (pathComposition C ⋙ F).map f.toPath

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: C : Type u
D : Type u₁
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
⊢ ∀ (a b : C) (e : a ⟶ b),
    (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).map e.toPath =
      eqToHom ⋯ ≫ (pathComposition C ⋙ F).map e.toPath ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.X₁.d j k = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V : Type u
inst✝ : Quiver V
⊢ ∀ {X Y : V} (f : X ⟶ Y),
    (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).map f.toPath ≫
        (Iso.refl ((Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).obj Y)).hom =
      (Iso.refl ((Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).obj X)).hom ≫ (𝟭 (Paths V)).map f.toPath

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V : Type u
inst✝ : Quiver V
⊢ ∀ (a b : V) (e : a ⟶ b),
    (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).map e.toPath =
      eqToHom ⋯ ≫ (𝟭 (Paths V)).map e.toPath ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Paths.of C ⋙q (pathComposition C).toPrefunctor = 𝟭q C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ (x₂ ≫ S.X₂.pOpcycles i) ≫ HomologicalComplex.opcyclesMap S.g i =
    (S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i) ≫ S.X₃.homologyι i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: ⊢ Functor.whiskerRight { app := fun x ↦ Paths.of ↑((𝟭 Quiv).obj x), naturality := adj._proof_1 } Cat.free ≫
      (Cat.free.associator forget Cat.free).hom ≫
        Cat.free.whiskerLeft { app := fun C ↦ (pathComposition ↑C).toCatHom, naturality := ⋯ } =
    NatTrans.id (𝟭 Quiv ⋙ Cat.free)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: ⊢ forget.whiskerLeft { app := fun x ↦ Paths.of ↑((𝟭 Quiv).obj x), naturality := adj._proof_1 } ≫
      (forget.associator Cat.free forget).inv ≫
        Functor.whiskerRight { app := fun C ↦ (pathComposition ↑C).toCatHom, naturality := ⋯ } forget =
    NatTrans.id (forget ⋙ 𝟭 Quiv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
F : Paths V ⥤ C
⊢ (fun G ↦ Cat.freeMap G ⋙ pathComposition C) ((fun F ↦ Paths.of V ⋙q F.toPrefunctor) F) = F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
G : V ⥤q C
⊢ (fun F ↦ Paths.of V ⋙q F.toPrefunctor) ((fun G ↦ Cat.freeMap G ⋙ pathComposition C) G) = G

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ S.X₁.liftCycles x₁ k hk ⋯ ≫ HomologicalComplex.cyclesMap S.f j = (x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij = S.X₁.liftCycles x₁ k hk ⋯ ≫ S.X₁.homologyπ j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
X Y : C
w : X ⟶ Y
hw : W w
⊢ (Paths.of (LocQuiver W)).obj { obj := Y } ⟶ (Paths.of (LocQuiver W)).obj { obj := X }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ {X Y : LocQuiver W} → (X ⟶ Y) → (G.obj X.obj ⟶ G.obj Y.obj)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (x y : Paths (LocQuiver W)) (f₁ f₂ : x ⟶ y),
    relations W f₁ f₂ → (liftToPathCategory G hG).map f₁ = (liftToPathCategory G hG).map f₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (X Y : C) (f : X ⟶ Y), (W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
⊢ ∀ (a b : LocQuiver W) (e : a ⟶ b),
    (Quotient.functor (relations W) ⋙ G₁).map e.toPath =
      eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map e.toPath ≫ eqToHom ⋯

Tactic:
· rintro ⟨X⟩ ⟨Y⟩ (f | ⟨w, hw⟩)
    · simpa only using! Functor.congr_hom h f
    · have hw : W.Q.map w = (wIso w hw).hom := rfl
      have hw' := Functor.congr_hom h w
      simp only [Functor.comp_map, hw] at hw'
      refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'
      all_goals apply Functor.congr_obj h

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
⊢ G₁ = G₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ Function.RightInverse (fun X ↦ X.as.obj) W.Q.obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
this : Localization.Construction.lift W.Q ⋯ = 𝟭 W.Localization
⊢ (Localization.Construction.lift W.Q ⋯).IsEquivalence

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
⊢ (Localization.Construction.lift W.Q ⋯).IsEquivalence

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
hW : W ≤ MorphismProperty.isomorphisms C
F : C ⥤ E
hF : W.IsInvertedBy F
⊢ 𝟭 C ⋙ F = F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
hW : W ≤ MorphismProperty.isomorphisms C
F₁ F₂ : C ⥤ E
eq : 𝟭 C ⋙ F₁ = 𝟭 C ⋙ F₂
⊢ F₁ = F₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization
⊢ W.Q ⋙ 𝟭 W.Localization = W.Q ⋙ Localization.Construction.lift L ⋯ ⋙ h₂.lift W.Q ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization
⊢ L ⋙ h₂.lift W.Q ⋯ ⋙ Localization.Construction.lift L ⋯ = L ⋙ 𝟭 D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
⊢ MorphismProperty.isomorphisms C ≤ MorphismProperty.isomorphisms C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this✝ : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
⊢ P f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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✝ : L.IsLocalization W
X : C
hX : W (𝟙 X)
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : W f
⊢ wIso f hf = isoOfHom W.Q W f hf

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
F : D ⥤ E
⊢ ((whiskeringLeft W.Localization D E).obj (equivalenceFromModel L W).functor ⋙
          (Construction.whiskeringLeftEquivalence W E).functor).obj
      F =
    (whiskeringLeftFunctor L W E).obj F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
⊢ ((whiskeringLeft W.Localization D E).obj (equivalenceFromModel L W).functor ⋙
            (Construction.whiskeringLeftEquivalence W E).functor).map
        τ ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (whiskeringLeftFunctor L W E).map τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
⊢ P = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E).IsEquivalence

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ app τ (W.Q.obj X) = τ.app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor' L W E).Full

Tactic:
by

Goal state after: