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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (h.ofExtend.extend e).hom i' j' = h.hom i' j'

Tactic:
·

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (h.ofExtend.extend e).hom i' j' = h.hom i' j'
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
k : ℕ
x : ↑(X k)
p q : ℤ
hpq : p + -1 = q
hp : p ≤ d + ↑k
⊢ p ≠ ↑k + d - 1 + 2

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsLE ((shiftFunctor C a).obj X) n' → t.IsLE X n

pp: case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsLE X n → t.IsLE ((shiftFunctor C a).obj X) n'

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsLE ((shiftFunctor C a).obj X) n' → t.IsLE X n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsLE X n → t.IsLE ((shiftFunctor C a).obj X) n'

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsLE X n → t.IsLE ((shiftFunctor C a).obj X) n'
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE ((shiftFunctor C a).obj X) n' → t.IsGE X n

pp: case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE X n → t.IsGE ((shiftFunctor C a).obj X) n'

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE ((shiftFunctor C a).obj X) n' → t.IsGE X n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE X n → t.IsGE ((shiftFunctor C a).obj X) n'

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE X n → t.IsGE ((shiftFunctor C a).obj X) n'
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ₁ φ₂ : (HomotopyCategory.quotient C c).obj K ⟶ (HomotopyCategory.quotient C c).obj L
hφ : (e.extendHomotopyFunctor C).map φ₁ = (e.extendHomotopyFunctor C).map φ₂
⊢ φ₁ = φ₂

Tactic:
obtain ⟨φ₁, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ₁

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ₂ : (HomotopyCategory.quotient C c).obj K ⟶ (HomotopyCategory.quotient C c).obj L
φ₁ : K ⟶ L
hφ : (e.extendHomotopyFunctor C).map ((HomotopyCategory.quotient C c).map φ₁) = (e.extendHomotopyFunctor C).map φ₂
⊢ (HomotopyCategory.quotient C c).map φ₁ = φ₂
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case hX
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this✝¹ : t.IsLE ((shiftFunctor C n₀).obj X) 0
this✝ : t.IsGE ((shiftFunctor C n₀).obj Y) (n₁ - n₀)
this : t.IsGE ((shiftFunctor C n₀).obj Y) 1
⊢ t.le 0 ((shiftFunctor C n₀).obj X)

pp: case hY
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this✝¹ : t.IsLE ((shiftFunctor C n₀).obj X) 0
this✝ : t.IsGE ((shiftFunctor C n₀).obj Y) (n₁ - n₀)
this : t.IsGE ((shiftFunctor C n₀).obj Y) 1
⊢ t.ge 1 ((shiftFunctor C n₀).obj Y)

Tactic:
·

Goal state after:
case hX
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this✝¹ : t.IsLE ((shiftFunctor C n₀).obj X) 0
this✝ : t.IsGE ((shiftFunctor C n₀).obj Y) (n₁ - n₀)
this : t.IsGE ((shiftFunctor C n₀).obj Y) 1
⊢ t.le 0 ((shiftFunctor C n₀).obj X)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ IsIso ((HomotopyCategory.quotient C c').map (extendMap f e)) ↔
    IsIso ((e.extendHomotopyFunctor C).map ((HomotopyCategory.quotient C c).map f))

Tactic:
change _ ↔ IsIso ((HomotopyCategory.quotient C c ⋙ e.extendHomotopyFunctor C).map f)

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ IsIso ((HomotopyCategory.quotient C c').map (extendMap f e)) ↔
    IsIso ((HomotopyCategory.quotient C c ⋙ e.extendHomotopyFunctor C).map f)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case hY
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this✝¹ : t.IsLE ((shiftFunctor C n₀).obj X) 0
this✝ : t.IsGE ((shiftFunctor C n₀).obj Y) (n₁ - n₀)
this : t.IsGE ((shiftFunctor C n₀).obj Y) 1
⊢ t.ge 1 ((shiftFunctor C n₀).obj Y)

Tactic:
·

Goal state after:
case hY
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this✝¹ : t.IsLE ((shiftFunctor C n₀).obj X) 0
this✝ : t.IsGE ((shiftFunctor C n₀).obj Y) (n₁ - n₀)
this : t.IsGE ((shiftFunctor C n₀).obj Y) 1
⊢ t.ge 1 ((shiftFunctor C n₀).obj Y)
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ n ≤ ↑k₀ + d - 1

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ n + 0 = n

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ n + 1 = n + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h✝ : K.IsStrictlyLE 0
⊢ 0 ≤ 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h✝ : K.IsStrictlyGE 1
⊢ 0 ≤ 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ 0 + 1 = 1

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ n + -1 = n - 1

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ n ≤ d + ↑k₀

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₁ ≫ e₂.hom =
    (Iso.refl (triangleOfSES h).obj₁).hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₁

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₂ ≫
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13))).hom =
    e₂.hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₂

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₁ ≫ e₂.hom =
    (Iso.refl (triangleOfSES h).obj₁).hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ n + 1 + -1 = n

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₂ ≫
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13))).hom =
    e₂.hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₂

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₂ ≫
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13))).hom =
    e₂.hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ n + 1 ≤ d + ↑k₀

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ X.IsGE n → ∀ i < n, IsZero ((homologyFunctor C i).obj X)

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ (∀ i < n, IsZero ((homologyFunctor C i).obj X)) → X.IsGE n

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ X.IsGE n → ∀ i < n, IsZero ((homologyFunctor C i).obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ (∀ i < n, IsZero ((homologyFunctor C i).obj X)) → X.IsGE n

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ (∀ i < n, IsZero ((homologyFunctor C i).obj X)) → X.IsGE n
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ X.IsLE n → ∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ (∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)) → X.IsLE n

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ X.IsLE n → ∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ (∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)) → X.IsLE n

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ (∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)) → X.IsLE n
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ -1 + n = m

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts.rlp ≤ T.rlp

pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.pushouts.rlp

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts.rlp ≤ T.rlp
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.pushouts.rlp

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.pushouts.rlp
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ (coproducts.{w, v, u} T).rlp ≤ T.rlp

pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ (coproducts.{w, v, u} T).rlp ≤ T.rlp
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ n.negOnePow • (n.negOnePow • (δ (-1) 0 f).rightUnshift n ⋯).rightShift n 0 ⋯ = δ (-1) 0 f

Tactic:
simp [smul_smul]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.retracts.rlp ≤ T.rlp

pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.retracts.rlp

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.retracts.rlp ≤ T.rlp
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.retracts.rlp

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.retracts.rlp
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = ↑(Cocycle.ofHom (𝟙 L))
⊢ n + -1 = m

Tactic:
by lia

Goal state after: