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
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m x✝² x✝¹ : ℤ
hij : ¬(ComplexShape.up ℤ).Rel x✝² x✝¹
x✝ : ↑(AddCommGrpCat.of (Cochain F G x✝²))
p✝ q✝ : ℤ
hpq✝ : p✝ + x✝¹ = q✝
⊢ Cochain.v ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝² x✝¹))) x✝) p✝ q✝ hpq✝ =
    Cochain.v ((AddCommGrpCat.Hom.hom 0) x✝) p✝ q✝ hpq✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m x✝² x✝¹ : ℤ
hij : ¬(ComplexShape.up ℤ).Rel x✝² x✝¹
x✝ : ↑(AddCommGrpCat.of (Cochain F G x✝²))
p✝ q✝ : ℤ
hpq✝ : p✝ + x✝¹ = q✝
⊢ Cochain.v ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝² x✝¹))) x✝) p✝ q✝ hpq✝ =
    Cochain.v ((AddCommGrpCat.Hom.hom 0) x✝) p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m x✝⁵ x✝⁴ x✝³ : ℤ
x✝² : (ComplexShape.up ℤ).Rel x✝⁵ x✝⁴
x✝¹ : (ComplexShape.up ℤ).Rel x✝⁴ x✝³
x✝ : ↑(AddCommGrpCat.of (Cochain F G x✝⁵))
p✝ q✝ : ℤ
hpq✝ : p✝ + x✝³ = q✝
⊢ Cochain.v
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝⁵ x✝⁴) ≫ AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝⁴ x✝³)))
        x✝)
      p✝ q✝ hpq✝ =
    Cochain.v ((AddCommGrpCat.Hom.hom 0) x✝) p✝ q✝ hpq✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m x✝⁵ x✝⁴ x✝³ : ℤ
x✝² : (ComplexShape.up ℤ).Rel x✝⁵ x✝⁴
x✝¹ : (ComplexShape.up ℤ).Rel x✝⁴ x✝³
x✝ : ↑(AddCommGrpCat.of (Cochain F G x✝⁵))
p✝ q✝ : ℤ
hpq✝ : p✝ + x✝³ = q✝
⊢ Cochain.v
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝⁵ x✝⁴) ≫ AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝⁴ x✝³)))
        x✝)
      p✝ q✝ hpq✝ =
    Cochain.v ((AddCommGrpCat.Hom.hom 0) x✝) p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₁ : ((inl φ).comp γ₁ ⋯).v (p + 1) q ⋯ = ((inl φ).comp γ₂ ⋯).v (p + 1) q ⋯
h₂ : ((Cochain.ofHom (inr φ)).comp γ₁ ⋯).v p q ⋯ = ((Cochain.ofHom (inr φ)).comp γ₂ ⋯).v p q ⋯
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.v p q hpq

Tactic:
simp only [Cochain.comp_v (inl φ) _ _ (p + 1) p q (by lia) hpq] at h₁

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₂ : ((Cochain.ofHom (inr φ)).comp γ₁ ⋯).v p q ⋯ = ((Cochain.ofHom (inr φ)).comp γ₂ ⋯).v p q ⋯
h₁ : (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.v p q hpq
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cochain F G n
⊢ z ∈ cocycle F G n ↔ δ n (n + 1) z = 0

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cochain F G n
⊢ z ∈ cocycle F G n ↔ δ n (n + 1) z = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (↑((x✝² * x✝¹) • x✝)).v p✝ q✝ hpq✝ = (↑(x✝² • x✝¹ • x✝)).v p✝ q✝ hpq✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (↑((x✝² * x✝¹) • x✝)).v p✝ q✝ hpq✝ = (↑(x✝² • x✝¹ • x✝)).v p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (x✝² * x✝¹) • (↑x✝).v p✝ q✝ hpq✝ = x✝² • x✝¹ • (↑x✝).v p✝ q✝ hpq✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (x✝² * x✝¹) • (↑x✝).v p✝ q✝ hpq✝ = x✝² • x✝¹ • (↑x✝).v p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ j + 1 = i

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ j + 1 = i
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ i + 1 = k

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ i + 1 = k
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (↑((x✝² + x✝¹) • x✝)).v p✝ q✝ hpq✝ = (↑(x✝² • x✝ + x✝¹ • x✝)).v p✝ q✝ hpq✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (↑((x✝² + x✝¹) • x✝)).v p✝ q✝ hpq✝ = (↑(x✝² • x✝ + x✝¹ • x✝)).v p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (x✝² + x✝¹) • (↑x✝).v p✝ q✝ hpq✝ = x✝² • (↑x✝).v p✝ q✝ hpq✝ + x✝¹ • (↑x✝).v p✝ q✝ hpq✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (x✝² + x✝¹) • (↑x✝).v p✝ q✝ hpq✝ = x✝² • (↑x✝).v p✝ q✝ hpq✝ + x✝¹ • (↑x✝).v p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel 0 0

Tactic:
;

Goal state after:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel 0 0
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0

Tactic:
;

Goal state after:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
l : s.pt ⟶ (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt
hl : l ≫ Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) = s.ι
x✝ : ↑s.pt
⊢ (AddCommGrpCat.Hom.hom l) x✝ =
    (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }))
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
l : s.pt ⟶ (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt
hl : l ≫ Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) = s.ι
x✝ : ↑s.pt
⊢ (AddCommGrpCat.Hom.hom l) x✝ =
    (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }))
      x✝
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
hi : ¬c.Rel i (c.next i)
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)

Tactic:
dsimp [mapHomologicalComplexObjXIso, XIso, inrX]
    simp [dif_neg hi]

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

Goal state before:
pp: case hnc
ι : 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✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i j : ℕ
w : ¬(ComplexShape.up ℕ).Rel j i
⊢ ¬j + 1 = i

Tactic:
;

Goal state after:
case hnc
ι : 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✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i j : ℕ
w : ¬(ComplexShape.up ℕ).Rel j i
⊢ ¬j + 1 = i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
h' : j + 1 = i
⊢ i + -1 = j

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
h' : j + 1 = i
⊢ i + -1 = j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ ↑((Cocycle.equivHom F G) f₁) = ↑((Cocycle.equivHom F G) f₂)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ ↑((Cocycle.equivHom F G) f₁) = ↑((Cocycle.equivHom F G) f₂)
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 : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
g : Y✝ ⟶ Z✝
f : HomotopyEquiv X✝ Y✝
e : HomotopyEquiv X✝ Z✝
he : e.hom = f.hom ≫ g
⊢ Homotopy (f.symm.trans e).hom g

Tactic:
simp only [HomotopyEquiv.trans_hom, HomotopyEquiv.symm_hom, he, ← Category.assoc]

Goal state after:
ι : 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 : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
g : Y✝ ⟶ Z✝
f : HomotopyEquiv X✝ Y✝
e : HomotopyEquiv X✝ Z✝
he : e.hom = f.hom ≫ g
⊢ Homotopy ((f.inv ≫ f.hom) ≫ g) g
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✝ : ι
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : F.Additive
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ F.map (h.hom i j) = 0

Tactic:
;

Goal state after:
ι : 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✝ : ι
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : F.Additive
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ F.map (h.hom i j) = 0
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.as = default.as

Tactic:
;

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
inst✝ : Unique C
a : Quotient r
⊢ a.as = default.as
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case pos
ι✝ : 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 : ι
h : c.Rel (c.prev i) i
⊢ f.f (c.prev i) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i) +
      g.f (c.prev i)

pp: case neg
ι✝ : 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 : ι
h : ¬c.Rel (c.prev i) i
⊢ f.f (c.prev i) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        (f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)

Tactic:
· rw [ho.comm (c.prev i)]
      dsimp [dFrom, dTo, fromNext, toPrev]
      rw [congr_arg (fun j => d K (c.prev i) j ≫ ho.hom j (c.prev i)) (c.next_eq' h)]

Goal state after:
case neg
ι✝ : 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 : ι
h : ¬c.Rel (c.prev i) i
⊢ f.f (c.prev i) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        (f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)
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₁ = lift r (functor r ⋙ F₂) ?m.62

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₂
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂

Tactic:
;

Goal state after:
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₁ = lift r (functor r ⋙ F₂) ?m.62

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₂
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂
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
  rw [lift_unique r (functor r ⋙ F₂) _ F₂ rfl]; swap
  · rintro X Y f g h
    dsimp
    rw [Quotient.sound r h]
  apply lift_unique
  rw [h]

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 τ₂
X : C
⊢ τ₁.app { as := X } = τ₂.app { as := X }

Tactic:
;

Goal state after:
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 τ₂
X : C
⊢ τ₁.app { as := X } = τ₂.app { as := X }
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk.mk.mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝³ : P ⟶ Q
a✝² : P.as ⟶ Q.as
b✝ : P ⟶ Q
a✝¹ : P.as ⟶ Q.as
c✝ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ Quot.mk (HomRel.CompClosure r) a✝² + Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝ =
    Quot.mk (HomRel.CompClosure r) a✝² + (Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝)

Tactic:
;

Goal state after:
case mk.mk.mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝³ : P ⟶ Q
a✝² : P.as ⟶ Q.as
b✝ : P ⟶ Q
a✝¹ : P.as ⟶ Q.as
c✝ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ Quot.mk (HomRel.CompClosure r) a✝² + Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝ =
    Quot.mk (HomRel.CompClosure r) a✝² + (Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝)
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 : Linear R (Quotient r) := linear R r hr
⊢ Functor.Linear R (functor r)

Tactic:
;

Goal state after:
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 : Linear R (Quotient r) := linear R r hr
⊢ Functor.Linear R (functor r)
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ 0 + Quot.mk (HomRel.CompClosure r) a✝ = Quot.mk (HomRel.CompClosure r) a✝

Tactic:
;

Goal state after:
case mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ 0 + Quot.mk (HomRel.CompClosure r) a✝ = Quot.mk (HomRel.CompClosure r) a✝
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ Quot.mk (HomRel.CompClosure r) a✝ + 0 = Quot.mk (HomRel.CompClosure r) a✝

Tactic:
;

Goal state after:
case mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ Quot.mk (HomRel.CompClosure r) a✝ + 0 = Quot.mk (HomRel.CompClosure r) a✝
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ -Quot.mk (HomRel.CompClosure r) a✝ + Quot.mk (HomRel.CompClosure r) a✝ = 0

Tactic:
;

Goal state after:
case mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ -Quot.mk (HomRel.CompClosure r) a✝ + Quot.mk (HomRel.CompClosure r) a✝ = 0