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

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X

pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ ∀ (X : Paths V), F.obj X = G.obj X

pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ ∀ (X : Paths V), F.obj X = G.obj X
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) Functor.ext._auto_1
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝

pp: case mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝

Tactic:
·

Goal state after:
case mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝

Tactic:
·

Goal state after:
case mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝

pp: case mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝

Tactic:
·

Goal state after:
case mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝

Tactic:
·

Goal state after:
case mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths p

pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths q

pp: case refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
x✝ : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths p
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths q

pp: case refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
x✝ : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths q
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case refine_1
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
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ ↑H ≫ S.X₁.d i (c.next i) = 0

pp: case refine_2
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
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ S.X₁.liftCycles (↑H) (c.next i) ⋯ ?refine_1 ≫ cyclesMap S.f i = k

Tactic:
·

Goal state after:
case refine_1
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
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ ↑H ≫ S.X₁.d i (c.next i) = 0
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
x✝ : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)

Tactic:
·

Goal state after:
case refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
x✝ : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
hp : W.paths p
h : W (𝟙 X)
⊢ W (composePath p)

Tactic:
revert hp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
h : W (𝟙 X)
⊢ W.paths p → W (composePath p)
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case nil
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
c✝ : C
f : X ⟶ c✝
hp : W.paths Path.nil → 0 < Path.nil.length → W (composePath Path.nil)
hp' : W.paths (Path.nil.cons f)
hp'' : 0 < (Path.nil.cons f).length
⊢ W (composePath (Path.nil.cons f))

pp: case cons
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
b✝¹ c✝ : C
f : b✝¹ ⟶ c✝
b✝ : C
a✝¹ : Path X b✝
a✝ : b✝ ⟶ b✝¹
hp : W.paths (a✝¹.cons a✝) → 0 < (a✝¹.cons a✝).length → W (composePath (a✝¹.cons a✝))
hp' : W.paths ((a✝¹.cons a✝).cons f)
hp'' : 0 < ((a✝¹.cons a✝).cons f).length
⊢ W (composePath ((a✝¹.cons a✝).cons f))

Tactic:
·

Goal state after:
case nil
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
c✝ : C
f : X ⟶ c✝
hp : W.paths Path.nil → 0 < Path.nil.length → W (composePath Path.nil)
hp' : W.paths (Path.nil.cons f)
hp'' : 0 < (Path.nil.cons f).length
⊢ W (composePath (Path.nil.cons f))
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case cons
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
b✝¹ c✝ : C
f : b✝¹ ⟶ c✝
b✝ : C
a✝¹ : Path X b✝
a✝ : b✝ ⟶ b✝¹
hp : W.paths (a✝¹.cons a✝) → 0 < (a✝¹.cons a✝).length → W (composePath (a✝¹.cons a✝))
hp' : W.paths ((a✝¹.cons a✝).cons f)
hp'' : 0 < ((a✝¹.cons a✝).cons f).length
⊢ W (composePath ((a✝¹.cons a✝).cons f))

Tactic:
·

Goal state after:
case cons
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
b✝¹ c✝ : C
f : b✝¹ ⟶ c✝
b✝ : C
a✝¹ : Path X b✝
a✝ : b✝ ⟶ b✝¹
hp : W.paths (a✝¹.cons a✝) → 0 < (a✝¹.cons a✝).length → W (composePath (a✝¹.cons a✝))
hp' : W.paths ((a✝¹.cons a✝).cons f)
hp'' : 0 < ((a✝¹.cons a✝).cons f).length
⊢ W (composePath ((a✝¹.cons a✝).cons f))
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case refine_2
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
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ S.X₁.liftCycles (↑H) (c.next i) ⋯ ⋯ ≫ cyclesMap S.f i = k

Tactic:
·

Goal state after:
case refine_2
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
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ S.X₁.liftCycles (↑H) (c.next i) ⋯ ⋯ ≫ cyclesMap S.f i = k
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
⊢ W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)

pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : W.paths.strictMap (pathComposition C) x✝¹
f✝ : x✝³ ⟶ x✝²
h : W.paths f✝
⊢ W.multiplicativeClosure ((pathComposition C).map f✝)

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
⊢ W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : W.paths.strictMap (pathComposition C) x✝¹
f✝ : x✝³ ⟶ x✝²
h : W.paths f✝
⊢ W.multiplicativeClosure ((pathComposition C).map f✝)

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : W.paths.strictMap (pathComposition C) x✝¹
f✝ : x✝³ ⟶ x✝²
h : W.paths f✝
⊢ W.multiplicativeClosure ((pathComposition C).map f✝)
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case pos
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)
⊢ { 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

pp: case neg
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)
⊢ { 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:
·

Goal state after:
case pos
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)
⊢ { 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
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case neg
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)
⊢ { 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:
·

Goal state after:
case neg
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)
⊢ { 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
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case inl
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
f : X.obj ⟶ Y.obj
⊢ G.obj X.obj ⟶ G.obj Y.obj

pp: case inr
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
g : Y.obj ⟶ X.obj
hg : W g
⊢ G.obj X.obj ⟶ G.obj Y.obj

Tactic:
·

Goal state after:
case inl
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
f : X.obj ⟶ Y.obj
⊢ G.obj X.obj ⟶ G.obj Y.obj
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case inr
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
g : Y.obj ⟶ X.obj
hg : W g
⊢ G.obj X.obj ⟶ G.obj Y.obj

Tactic:
·

Goal state after:
case inr
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
g : Y.obj ⟶ X.obj
hg : W g
⊢ G.obj X.obj ⟶ G.obj Y.obj
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_1
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₂
⊢ ∀ (X : W.Localization), G₁.obj X = G₂.obj X

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₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X Y : W.Localization) (f : X ⟶ Y), G₁.map f = eqToHom ⋯ ≫ G₂.map f ≫ eqToHom ⋯

Tactic:
·

Goal state after:
case refine_1
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₂
⊢ ∀ (X : W.Localization), G₁.obj X = G₂.obj X
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₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X Y : W.Localization) (f : X ⟶ Y), G₁.map f = eqToHom ⋯ ≫ G₂.map f ≫ eqToHom ⋯

Tactic:
·

Goal state after:
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₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X Y : W.Localization) (f : X ⟶ Y), G₁.map f = eqToHom ⋯ ≫ G₂.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_1
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₂
⊢ (Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj

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:
·

Goal state after:
case refine_1
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₂
⊢ (Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj
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:
·

Goal state after:
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 ⋯
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_2.inl
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₂
X Y : C
f : { obj := X }.obj ⟶ { obj := Y }.obj
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inl f)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inl f)) ≫ eqToHom ⋯

pp: case refine_2.inr
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₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw : W w
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) ≫ eqToHom ⋯

Tactic:
·

Goal state after:
case refine_2.inl
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₂
X Y : C
f : { obj := X }.obj ⟶ { obj := Y }.obj
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inl f)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inl f)) ≫ eqToHom ⋯