mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ f + g + h' = f + (g + h')

Tactic:
by
    ext
    apply add_assoc

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.p.app j ≫ P.X.map φ ≫ (f.app j').f

Tactic:
← P.p.naturality_assoc

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.castSucc) =
    X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.succ)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_δ_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)

Tactic:
simp only [skeletalFunctor_obj, skeletalFunctor_map,
    NonemptyFinLinOrd.mono_iff_injective, NonemptyFinLinOrd.coe_of, ConcreteCategory.hom_ofHom]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : ¬y = i
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) y)

Tactic:
· dsimp [δ]
      rw [Fin.succAbove_of_le_castSucc i.succ _]
      simp only [Fin.lt_def, Fin.le_iff_val_le_val, Fin.val_succ, Fin.val_castSucc,
        Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢
      lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

pp: case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Tactic:
· exact ⟨x, y, ⟨h₁, h⟩⟩

Goal state after:
case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s : X.S
d : ℕ
hd : s.dim = d
⊢ X _⦋s.dim⦌ = X _⦋d⦌

Tactic:
by simp only [hd]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ f = Pi.lift fun j ↦ s.π.app (some j)

Tactic:
by
        dsimp
        ext j
        dsimp only [Limits.Pi.lift]
        rw [limit.lift_π]
        dsimp
        rw [← h (some j)]

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x✝ : ↥{a, b, c}
x : α
hx : x ∈ {a, b, c}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
by
      simp only [Finset.mem_insert, Finset.mem_singleton] at hx
      obtain rfl | rfl | rfl := hx
      · exact ⟨0, rfl⟩
      · exact ⟨1, rfl⟩
      · exact ⟨2, rfl⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
⊢ ((if hij : c.Rel i j then if hi : Even i then φ else ψ else 0) ≫
      if hij : c.Rel j k then if hi : Even j then φ else ψ else 0) =
    0

Tactic:
split_ifs with hi hj hj

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : Even i
hj : Even j
⊢ φ ≫ φ = 0

case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : Even i
hj : ¬Even j
⊢ φ ≫ ψ = 0

case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : Even j
⊢ ψ ≫ φ = 0

case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : ¬Even j
⊢ ψ ≫ ψ = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n m : ℕ
x✝ : { x // x ∈ Δ[n].nonDegenerate m }
x : Δ[n] _⦋m⦌
hx : x ∈ Δ[n].nonDegenerate m
⊢ #(Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ) = m + 1

Tactic:
rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective] at hx

Goal state after:
n m : ℕ
x✝ : { x // x ∈ Δ[n].nonDegenerate m }
x : Δ[n] _⦋m⦌
hx : Function.Injective ⇑(Hom.toOrderHom (objEquiv x))
⊢ #(Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ) = m + 1
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))

Tactic:
apply Associative.assoc

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      d₁ i₁ i₁' i ≫ { X := fun i₂ ↦ X (i₁', i₂), d := fun i₂ i₂' ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i j =
        { X := fun i₂ ↦ X (i₁, i₂), d := fun i₂ i₂' ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i j ≫ d₁ i₁ i₁' j

Tactic:
intros; apply comm

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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']; swap
        · rw [← ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
        by_cases h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
        · rw [totalAux.d₁_eq K c₁₂ h₄ i₂ i₁₂'', Linear.comp_units_smul,
            d_f_comp_d_f_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₁ c₂ c₁₂ h₄, ← ComplexShape.next_π₁ c₂ c₁₂ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₁_eq_zero _ _ _ _ h₄, comp_zero, smul_zero]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂
⊢ c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂

Tactic:
by rw [h₁, h₂, h]

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

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
hj' : c₁.π c₂ c (i₁, c₂.prev i₂) = j'
hi₂ : c₂.Rel (c₂.prev i₂) i₂
⊢ c₁.ε₂ c₂ c (i₁, c₂.prev i₂) •
      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂)) ≫ L₁.ιMapBifunctor L₂ F c i₁ (c₂.prev i₂) j' hj' =
    (c₁.σ c₂ c i₁ i₂ * c₂.ε₁ c₁ c (c₂.prev i₂, i₁) * c₁.σ c₂ c i₁ (c₂.prev i₂)) •
      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂)) ≫ L₁.ιMapBifunctor L₂ F c i₁ (c₂.prev i₂) j' ⋯

Tactic:
congr 1
        nth_rw 2 [mul_comm]
        rw [← ComplexShape.σ_ε₂ c₁ c i₁ hi₂, mul_comm, ← mul_assoc,
          Int.units_mul_self, one_mul]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ (shiftFunctor C 1).obj Y₁
hT : Triangle.mk f h g ∈ distinguishedTriangles
hY₁ : P Y₁
α : X ⟶ Y₃
⊢ ∃ a, (fun f ↦ f ≫ h) a = α

Tactic:
obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ (rot_of_distTriang _ hT)
        α (hX _ (P.le_shift _ _ hY₁))

Goal state after:
case refine_2.refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ (shiftFunctor C 1).obj Y₁
hT : Triangle.mk f h g ∈ distinguishedTriangles
hY₁ : P Y₁
β : X ⟶ (Triangle.mk f h g).rotate.obj₁
⊢ ∃ a, (fun f ↦ f ≫ h) a = β ≫ (Triangle.mk f h g).rotate.mor₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
hL : (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0

Tactic:
← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
hL : (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0
Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKInjective
inst✝ : L.IsKInjective
f : K ⟶ L
x✝ : QuasiIso f
⊢ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKInjective
inst✝ : L.IsKInjective
f : K ⟶ L
x✝ : QuasiIso f
⊢ IsIso ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f)
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
⊢ Nonempty (Homotopy f 0)

Tactic:
by
    /- The strategy of the proof is express the `0`-cocycle in `Cochain K L 0`
    corresponding to `f` as the coboundary of a `-1`-cochain. An approximate
    solution for some `n : ℕ` is an element in the subset `X n` consisting
    of the `-1`-cochains such that `δ (-1) 0 α` coincide with `Cochain.ofHom f`
    up to the degree `n + d - 1`. The assumption on `L` implies that
    the zero `-1`-cochain belongs to `X 0`, and we use the lemma
    `isKInjective_of_injective_aux` in order to get better approximations,
    and we pass to the limit. -/
    let X (n : ℕ) : Set (Cochain K L (-1)) :=
      Set.ofPred (fun α => (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (n + d - 1))
    let x₀ : X 0 := ⟨0, fun p q hpq hp ↦
      IsZero.eq_of_tgt (L.isZero_of_isStrictlyGE d _ (by lia)) _ _⟩
    let φ (n : ℕ) (α : X n) : X (n + 1) :=
      ⟨_, (isKInjective_of_injective_aux f α.1 (n + d - 1) ((n + 1 : ℕ) + d - 1)
        (by lia) (hK _) α.2).choose_spec⟩
    have hφ (k : ℕ) (x : X k) : (φ k x).1.EqUpTo x.1 (d + k) := fun p q hpq hp => by
      dsimp [φ]
      rw [add_eq_left, Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
    refine ⟨(Cochain.equivHomotopy f 0).symm ⟨limitSequence φ hφ x₀, ?_⟩⟩
    rw [Cochain.ofHom_zero, add_zero]
    ext n
    let k₀ := (n - d + 1).toNat
    rw [← (sequence φ x₀ k₀).2 n n (add_zero n) (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ n (n - 1) (by lia) (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ (n + 1) n (by lia) (by lia)]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj K) ↔ CochainComplex.plus C K

Tactic:
by
  refine ⟨?_, fun h ↦ ⟨_, h⟩⟩
  simp only [plus, ObjectProperty.strictMap_iff]
  rintro ⟨L, h, hL⟩
  obtain rfl : L = K := congr_arg Quotient.as hL
  exact h

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map (w₂₃.unop ≫ o.m₁)).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂ =
    (((shiftFunctor C 1).map w₁₃.unop).op ≫ ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map u₁₂).unop).op) ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso,

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map (w₂₃.unop ≫ o.m₁)).op =
    ((shiftFunctor C 1).map w₁₃.unop).op ≫ ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map u₁₂).unop).op
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
X Y : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst✝ : Mono i
I : C
w✝ : Injective I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs }.Splitting
hI : (MorphismProperty.monomorphisms C).rlp 0
t : PullbackCone 0 0
⊢ (t.fst ≫ s + t.snd ≫ σ.s) ≫ p = t.snd

Tactic:
by simp [hs, dsimp% σ.s_g]

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip✝ : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
⊢ sq.HasLift

Tactic:
have (n : ℤ) : Injective ((kernel p).X n) :=
      Injective.of_iso
        (asIso (kernelComparison p (HomologicalComplex.eval _ _ n))).symm (hp n).2

Goal state after:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip✝ : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this : ∀ (n : ℤ), Injective ((kernel p).X n)
⊢ sq.HasLift
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
⊢ (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK)).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)

Tactic:
by
  ext n m hnm
  simp [cocycle₁]

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ IsIso ((π K L n₁).f i)

Tactic:
refine ⟨(biprod.inr : _ ⟶ mid K L n₁).f i, ?_, by simp⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ (π K L n₁).f i ≫ biprod.inr.f i = 𝟙 ((mid K L n₁).X i)