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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
⊢ (H.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ H).hom =
    inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
⊢ CompClosure r m₁ m₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, CompClosure r g g' → CompClosure r (f ≫ g) (f ≫ g')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
⊢ ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z), CompClosure r f f' → CompClosure r (f ≫ g) (f' ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
inst✝¹ : IsStableUnderPrecomp r
inst✝ : IsStableUnderPostcomp r
X Y : C
f g : X ⟶ Y
⊢ CompClosure r f g ↔ r f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
inst✝¹ : IsStableUnderPrecomp r
inst✝ : IsStableUnderPostcomp r
⊢ CompClosure r = r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, F.homRel g g' → F.homRel (f ≫ g) (f ≫ g')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
⊢ ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z), F.homRel f f' → F.homRel (f ≫ g) (f' ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
X✝ Y✝ : C
⊢ ∀ {x y : X✝ ⟶ Y✝}, F.homRel x y → F.homRel y x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C✝ : Type u_1
inst✝² : Category.{v_1, u_1} C✝
r : HomRel C✝
C : Type u_2
D : Type u_3
inst✝¹ : Category.{v_2, u_2} C
inst✝ : Category.{v_3, u_3} D
F : C ⥤ D
X✝ Y✝ : C
⊢ ∀ {x y z : X✝ ⟶ Y✝}, F.homRel x y → F.homRel y z → F.homRel x z

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 K.cylinder

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
X✝ Y✝ : Quotient r
f : Hom r X✝ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as),
    comp r (Quot.mk (HomRel.CompClosure r) (𝟙 X✝.as)) (Quot.mk (HomRel.CompClosure r) a) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
X✝ Y✝ : Quotient r
f : Hom r X✝ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as),
    comp r (Quot.mk (HomRel.CompClosure r) a) (Quot.mk (HomRel.CompClosure r) (𝟙 Y✝.as)) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₀ K ≫ π K = 𝟙 K

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
⊢ (((shortComplexFunctor C c i).obj K).g ≫
      if c.Rel i (c.next i) then K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i)
      else f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) =
    0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
W✝ X✝ Y✝ Z✝ : Quotient r
f : Hom r W✝ X✝
g : Hom r X✝ Y✝
h : Hom r Y✝ Z✝
⊢ ∀ (a : Y✝.as ⟶ Z✝.as) (a_1 : X✝.as ⟶ Y✝.as) (a_2 : W✝.as ⟶ X✝.as),
    comp r (comp r (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_1))
        (Quot.mk (HomRel.CompClosure r) a) =
      comp r (Quot.mk (HomRel.CompClosure r) a_2)
        (comp r (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₀ K = ι₁ K ≫ π K ≫ ι₀ K

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₁ K ≫ 𝟙 K.cylinder = ι₁ K

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r✝ : HomRel C
G : Type u_2
inst✝ : Groupoid G
r : HomRel G
X Y : Quotient r
f : X ⟶ Y
x✝¹ x✝ : X.as ⟶ Y.as
con : HomRel.CompClosure r x✝¹ x✝
⊢ Quot.mk (HomRel.CompClosure r) (Groupoid.inv x✝¹) = Quot.mk (HomRel.CompClosure r) (Groupoid.inv x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r✝ : HomRel C
G : Type u_2
inst✝ : Groupoid G
r : HomRel G
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) ≫ Quot.mk (HomRel.CompClosure r) a = 𝟙 Y✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r✝ : HomRel C
G : Type u_2
inst✝ : Groupoid G
r : HomRel G
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), Quot.mk (HomRel.CompClosure r) a ≫ Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) = 𝟙 X✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : Linear R C
r : HomRel C
inst✝ : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as ⟶ Y.as
h₁₂ : HomRel.CompClosure r f₁ f₂
⊢ Quot.mk (HomRel.CompClosure r) (a • f₁) = Quot.mk (HomRel.CompClosure r) (a • f₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ (a * b) • f = a • b • f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝³ : DecidableRel c.Rel
inst✝² : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝¹ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
D : Type u_3
inst✝ : Category.{v_2, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
⊢ H.map (ι₀ K) = H.map (ι₁ K)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
X✝ Y✝ : C
f : (functor r).obj X✝ ⟶ (functor r).obj Y✝
⊢ (functor r).map (Quot.out f) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
inst✝ : Unique C
a : Quotient r
⊢ a = default

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
⊢ ∀ {a b : Quotient r} (f : a ⟶ b), P f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b : C
f₁ f₂ : a ⟶ b
h : r f₁ f₂
⊢ (functor r).map f₁ = (functor r).map f₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ 1 • f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' ↔ r f f'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
⊢ Congruence fun X Y ↦ Relation.EqvGen (HomRel.CompClosure r)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
⊢ a • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X✝ Y✝ : Quotient r
hf : X✝ ⟶ Y✝
⊢ ∀ (a b : X✝.as ⟶ Y✝.as), HomRel.CompClosure r a b → F.map a = F.map b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ {X Y Z : Quotient r} (f : X ⟶ Y) (g : Y ⟶ Z),
    Quot.liftOn (f ≫ g) (fun f ↦ F.map f) ⋯ = Quot.liftOn f (fun f ↦ F.map f) ⋯ ≫ Quot.liftOn g (fun f ↦ F.map f) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ functor r ⋙ lift r F H = F

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
⊢ ((shortComplexFunctor C c i).map f).τ₁ =
    (((shortComplexFunctor C c i).obj K).f ≫ ho.hom i (c.prev i) +
        if c.Rel (c.prev i) i then ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i)
        else f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      ((shortComplexFunctor C c i).map g).τ₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
f g : (functor r).obj X ⟶ (functor r).obj Y
⊢ a • (f + g) = a • f + a • g

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹¹ : HasHomotopyCofiber φ
inst✝¹⁰ : DecidableRel c.Rel
inst✝⁹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝⁸ : K.HasCylinder
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
H : C ⥤ D
inst✝⁵ : H.Additive
inst✝⁴ : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
inst✝² :
  ∀ (i : ι), HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i) (((H.mapHomologicalComplex c).obj F).X i)
inst✝¹ :
  HasHomotopyCofiber (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ (Iso.refl (Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).left).hom ≫
      (Arrow.mk (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))).hom =
    (Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).hom ≫
      ((H.mapHomologicalComplex c).mapBiprod F F).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
Φ : Quotient r ⥤ D
hΦ : functor r ⋙ Φ = F
⊢ Φ = lift r F H

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ (a + b) • f = a • f + b • f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ 0 • f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = F₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : Quotient r ⥤ D
τ₁ τ₂ : F ⟶ G
h : (functor r).whiskerLeft τ₁ = (functor r).whiskerLeft τ₂
⊢ τ₁.app = τ₂.app

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ⟶ functor r ⋙ G
x✝¹ x✝ : Quotient r
X Y : C
⊢ ∀ (f : { as := X } ⟶ { as := Y }),
    (F.map f ≫
        match { as := Y } with
        | { as := X } => τ.app X) =
      (match { as := X } with
        | { as := X } => τ.app X) ≫
        G.map f

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
⊢ ((shortComplexFunctor C c i).map f).τ₃ =
    (if c.Rel i (c.next i) then K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i)
        else f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        ho.hom (c.next i) i ≫ ((shortComplexFunctor C c i).obj L).g +
      ((shortComplexFunctor C c i).map g).τ₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G H : Quotient r ⥤ D
τ : functor r ⋙ F ⟶ functor r ⋙ G
τ' : functor r ⋙ G ⟶ functor r ⋙ H
⊢ natTransLift r τ ≫ natTransLift r τ' = natTransLift r (τ ≫ τ')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : Quotient r ⥤ D
⊢ natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r τ.hom ≫ natTransLift r τ.inv = 𝟙 F

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝² : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap h.hom i ≫ homologyMap h.inv i = 𝟙 (K.homology i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r τ.inv ≫ natTransLift r τ.hom = 𝟙 G

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝² : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap h.inv i ≫ homologyMap h.hom i = 𝟙 (L.homology i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X✝ Y✝ : Quotient r ⥤ D
f :
  ((whiskeringLeft C (Quotient r) D).obj (functor r)).obj X✝ ⟶
    ((whiskeringLeft C (Quotient r) D).obj (functor r)).obj Y✝
⊢ ((whiskeringLeft C (Quotient r) D).obj (functor r)).map (natTransLift r f) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ {X Y : Quotient r ⥤ D}, Function.Injective ((whiskeringLeft C (Quotient r) D).obj (functor r)).map

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.Full
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.Full
⊢ ∀ {X Y : Quotient L.homRel}, Function.Surjective (Quotient.lift L.homRel L ⋯).map

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
L : C ⥤ D
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
⊢ ∀ (X Y Z : Quotient r) (r_1 : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r_1 • f) ≫ g = r_1 • f ≫ g

Tactic:
by

Goal state after: