mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ i ≫ δ j.succ)) k) = ↑((Hom.toOrderHom (δ j ≫ δ i.castSucc)) k)

Tactic:
dsimp [δ, Fin.succAbove]

Goal state after:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ ↑(if (if k.castSucc < i then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < i then k.castSucc else k.succ).castSucc
      else (if k.castSucc < i then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < i.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h.right
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
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
⊢ e ≫ i = p

Tactic:
ext j
    simp [Y, i, e]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)

Tactic:
dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_succ, op_id, X.map_id]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (δ i)

Tactic:
rw [mono_iff_injective]
  exact Fin.succAbove_right_injective

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

Goal state before:
pp: i n m : ℕ
hi : n + i = m
x✝² x✝¹ : Fin (⦋m⦌.len + 1)
x✝ : x✝² ≤ x✝¹
⊢ (fun j ↦ if ↑j < i then 0 else ⟨↑j - i, ⋯⟩) x✝² ≤ (fun j ↦ if ↑j < i then 0 else ⟨↑j - i, ⋯⟩) x✝¹

Tactic:
by grind [Fin.zero_le]

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

Goal state before:
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:
refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩

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
⊢ y < x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ θ = σ i

Tactic:
rw [h, eq_id_of_epi θ', Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

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

Tactic:
obtain ⟨d, _, rfl⟩ := s.mk_surjective

Goal state after:
X : SSet
d✝ d : ℕ
w✝ : X _⦋d⦌
hd : { dim := d, simplex := w✝ }.dim = d✝
⊢ { dim := d, simplex := w✝ }.cast hd = { dim := d, simplex := w✝ }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map (𝟙 (op ⦋m₁⦌)))) ↑y₁ = ↑y₁

Tactic:
CategoryTheory.Functor.map_id,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (𝟙 (X _⦋m₁⦌))) ↑y₁ = ↑y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
⊢ ∃ hf₁, (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x

Tactic:
let α (y : Fin (m + 1)) : Fin (n + 1) :=
    if y = f₁.toOrderHom x then x else hf.section_.toOrderHom y

Goal state after:
X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
⊢ ∃ hf₁, (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
A : X.Subcomplex
d : ℕ
h✝ : X.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Function.Injective fun a ↦ ↑↑a

Tactic:
rintro ⟨⟨x, _⟩, _⟩ ⟨⟨y, _⟩, _⟩ rfl

Goal state after:
X : SSet
inst✝ : X.Finite
A : X.Subcomplex
d : ℕ
h✝ : X.HasDimensionLT d
i : ℕ
hi : i < d
x : X _⦋i⦌
property✝³ : x ∈ A.obj (Opposite.op ⦋i⦌)
property✝² : ⟨x, property✝³⟩ ∈ A.toSSet.nonDegenerate i
property✝¹ : (fun a ↦ ↑↑a) ⟨⟨x, property✝³⟩, property✝²⟩ ∈ A.obj (Opposite.op ⦋i⦌)
property✝ : ⟨(fun a ↦ ↑↑a) ⟨⟨x, property✝³⟩, property✝²⟩, property✝¹⟩ ∈ A.toSSet.nonDegenerate i
⊢ ⟨⟨x, property✝³⟩, property✝²⟩ = ⟨⟨(fun a ↦ ↑↑a) ⟨⟨x, property✝³⟩, property✝²⟩, property✝¹⟩, property✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_zero]
    simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_2
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ x✝¹ = x✝

Tactic:
exact ((Fin.succAboveOrderEmb (i.castPred (Fin.ne_last_of_lt h))).trans
        (Fin.succAboveOrderEmb j)).injective (by rwa [Subtype.ext_iff] at hk)

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) = 0

Tactic:
by
        dsimp
        rw [K₁.shape _ _ h₁, Functor.map_zero, zero_app]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Associator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
by
  dsimp [mapBifunctorAssociator]
  rw [ι_mapBifunctorComp₁₂MapObjIso_inv_assoc, ιMapTrifunctorMapObj,
    ι_mapMap_assoc, mapTrifunctorMapNatTrans_app_app_app]
  erw [ι_mapBifunctorComp₂₃MapObjIso_hom]

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₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

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₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ?pos✝) ≫
      K.D₂ c₁₂ i₁₂' i₁₂'' =
    0

Tactic:
· rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, ← c₁₂.next_eq' h₁, h]

Goal state after:
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₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ⋯) ≫
      K.D₂ c₁₂ i₁₂' i₁₂'' =
    0
Module: Mathlib.Algebra.Homology.BifunctorFlip

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹³ : Category.{v_1, u_1} C₁
inst✝¹² : Category.{v_2, u_2} C₂
inst✝¹¹ : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹⁰ : HasZeroMorphisms C₁
inst✝⁹ : HasZeroMorphisms C₂
inst✝⁸ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
φ₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex C₂ c₂
φ₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
inst✝⁶ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝⁵ : TotalComplexShape c₁ c₂ c
inst✝⁴ : TotalComplexShape c₂ c₁ c
inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝² : DecidableEq J
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
⊢ K₂.HasMapBifunctor K₁ F.flip c

Tactic:
rw [hasMapBifunctor_flip_iff]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹³ : Category.{v_1, u_1} C₁
inst✝¹² : Category.{v_2, u_2} C₂
inst✝¹¹ : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹⁰ : HasZeroMorphisms C₁
inst✝⁹ : HasZeroMorphisms C₂
inst✝⁸ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
φ₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex C₂ c₂
φ₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
inst✝⁶ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝⁵ : TotalComplexShape c₁ c₂ c
inst✝⁴ : TotalComplexShape c₂ c₁ c
inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝² : DecidableEq J
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
⊢ K₁.HasMapBifunctor K₂ F c
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
⊢ (CochainComplex.plus C).limitsOfShape J ≤ CochainComplex.plus C

Tactic:
rintro K ⟨p⟩

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
⊢ CochainComplex.plus C K
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
⊢ (CochainComplex.plus C).colimitsOfShape J ≤ CochainComplex.plus C

Tactic:
rintro K ⟨p⟩

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
⊢ CochainComplex.plus C K
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
Y : C
hY : P.trW.isLocal Y
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.RightFraction X Y
hφ : g = φ.map L ⋯
α : X ⟶ Y
hα : (fun g ↦ φ.s ≫ g) α = φ.f
⊢ L.map α = g

Tactic:
hφ,

Goal state after:
case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
Y : C
hY : P.trW.isLocal Y
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.RightFraction X Y
hφ : g = φ.map L ⋯
α : X ⟶ Y
hα : (fun g ↦ φ.s ≫ g) α = φ.f
⊢ L.map α = φ.map L ⋯
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
X : C
hX : P.trW.isColocal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.LeftFraction X Y
hφ : g = φ.map L ⋯
α : X ⟶ Y
hα : (fun f ↦ f ≫ φ.s) α = φ.f
⊢ L.map α = g

Tactic:
hφ,

Goal state after:
case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
X : C
hX : P.trW.isColocal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.LeftFraction X Y
hφ : g = φ.map L ⋯
α : X ⟶ Y
hα : (fun f ↦ f ≫ φ.s) α = φ.f
⊢ L.map α = φ.map L ⋯
Module: Mathlib.Algebra.Homology.HomotopyFiber

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.HasPathObject
i : α
h₁ : IsZero (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)
⊢ IsZero (op (K.pathObject.1 i))

Tactic:
dsimp [pathObject]

Goal state after:
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.HasPathObject
i : α
h₁ : IsZero (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)
⊢ IsZero (homotopyCofiber.X (biprod.lift (𝟙 K.op) (-𝟙 K.op)) i)
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
X✝ Y✝ Z W : C
f✝ : X✝ ⟶ Y✝
s : X✝ ⟶ Z
g : Z ⟶ W
t✝ : Y✝ ⟶ W
J : Type u_2
A B : J → C
inst✝² : HasCoproduct A
inst✝¹ : HasCoproduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty (f j) p
t : ∐ A ⟶ X
b : ∐ B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
⊢ sq.HasLift

Tactic:
have sq' (j : J) :
        CommSq (Sigma.ι _ j ≫ t) (f j) p (Sigma.ι _ j ≫ b) :=
      ⟨by simp [sq.w]⟩
    exact ⟨⟨{ l := Sigma.desc (fun j ↦ (sq' j).lift) }⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y : C
f : X ⟶ Y
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : IsIso f
⊢ Fibration f

Tactic:
by
  have := (cofibrations C).rlp_of_isIso f
  rw [cofibrations_rlp] at this
  simpa only [fibration_iff] using this.1

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₁ ≫ ObjectProperty.homMk h.h = g

Tactic:
ext; exact h.h₁

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk h.h ≫ Q.p₁ = g

Tactic:
ext; exact h.h₁

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
by
  obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
  obtain ⟨Q, _⟩ := PathObject.exists_very_good Z
  have sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) := { }
  exact ⟨Q,
   ⟨{ h := h.h ≫ sq.lift
      h₀ := by
        have := sq.fac_right =≫ prod.fst
        simp only [Category.assoc, prod.lift_fst, Q.p_fst] at this
        simp [this]
      h₁ := by
        have := sq.fac_right =≫ prod.snd
        simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this
        simp [this]
    }⟩⟩

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

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ (ι.obj X).IsGE n → X.IsGE n

pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ X.IsGE n → (ι.obj X).IsGE n

Tactic:
all_goals exact fun h ↦ ⟨h.1⟩

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

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ (ι.obj X).IsLE n → X.IsLE n

pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ X.IsLE n → (ι.obj X).IsLE n

Tactic:
all_goals exact fun h ↦ ⟨h.1⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ ((singleFunctor C n).obj X).IsLE n

Tactic:
← isLE_ι_obj_iff

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ (ι.obj ((singleFunctor C n).obj X)).IsLE n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₁ = TriangleMorphism.hom₁ 0

pp: case h₂
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₂ = TriangleMorphism.hom₂ 0

pp: case h₃
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0

Tactic:
· obtain ⟨g, hg⟩ := Triangle.coyoneda_exact₂ _ (inv_rot_of_distTriang _ hT')
      f.hom₁ (by simp [← f.comm₁, hf])
    simp [hg, t.zero_of_isLE_of_isGE g a (b + 1) (by lia)
      h₀ (t.isGE_shift _ b (-1) (b + 1))]

Goal state after:
case h₂
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₂ = TriangleMorphism.hom₂ 0

case h₃
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncLTι n₁).app X) ↔ IsZero ((t.truncGE n₁).obj X)

Tactic:
exact (Triangle.isZero₃_iff_isIso₁ _ (t.triangleLTGE_distinguished n₁ X)).symm

Goal state after: