mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx⟩
⊢ IsIso f

Tactic:
| _ m
   => 

Goal state after:
case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx⟩
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
x : A.toSSet _⦋n⦌
⊢ x ∈ A.toSSet.degenerate n ↔ x ∈ ⊤

Tactic:
simpa [A.mem_degenerate_iff] using h x.prop

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ x ∈ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)

Tactic:
simp only [Subfunctor.iSup_obj, Set.mem_iUnion, Sigma.exists,
    Subtype.exists, exists_prop]

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ ∃ a, ∃ a_1 ∈ X.nonDegenerate a, x ∈ (ofSimplex a_1).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)

Tactic:
rw [h_eq_assoc _ _ 0, X.left.σ₀Iter_δ' _ _ 1 (by grind),
      ed.s₀_comp_δ₁_assoc, X.δ₀Iter_hom_app_assoc _ (by grind)]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ X.hom.app (op ⦋n⦌) ≫ ed.s' ≫ X.left.σ₀Iter ↑(Fin.last n) ⋯ = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
| c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
ε₂_ε₁ c₁₂ h₁ h₂

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
| -c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
⊢ ∀ (p q : ℤ),
    (up ℤ).Rel p q →
      (MonoidHom.mk' Int.negOnePow Int.negOnePow_add) q = -(MonoidHom.mk' Int.negOnePow Int.negOnePow_add) p

Tactic:
by
    rintro p _ rfl
    dsimp
    rw [Int.negOnePow_succ]

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

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_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : 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
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j

Tactic:
rw [← h, ← ρ₁₂.hpq]

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

Goal state before:
pp: 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₂ : K₂ ⟶ L₂
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)

Tactic:
rintro X Y a b _ d _ _ rfl rfl rfl

Goal state after:
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₂ : K₂ ⟶ L₂
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
X Y : D
a b d : X ⟶ Y
⊢ a + b = a + d + (b + -d)
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₂ : K₂ ⟶ L₂
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
        (F.map (L₁.d (c₁.prev i₁) i₁)).app (L₂.X i₂) ≫
          (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h

Tactic:
NatTrans.naturality_assoc

Goal state after:
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₂ : K₂ ⟶ L₂
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
⊢ (commShiftIso ((F ⋙ G).obj ((shiftFunctor C₁' m).obj X₁')) n).hom.app X₂ ≫
      (shiftFunctor D n).map ((commShiftIso ((F ⋙ G).flip.obj X₂) m).hom.app X₁') =
    (commShiftIso ((F ⋙ G).flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app X₁' ≫
      (shiftFunctor D m).map ((commShiftIso ((F ⋙ G).obj X₁') n).hom.app X₂) ≫
        (shiftComm (((F ⋙ G).obj X₁').obj X₂) m n).inv ≫
          (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj (((F ⋙ G).obj X₁').obj X₂)))

Tactic:
have := G.commShift₂_comm h (F.obj X₁') X₂ m n
    dsimp [commShiftIso] at this ⊢
    simp only [Category.comp_id, Category.id_comp, map_comp, Category.assoc]
    rw [NatTrans.shift_app (G.map ((F.commShiftIso m).hom.app X₁')) n X₂]
    simp [this]

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

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ biprod.inl ≫ biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ =
    biprod.inl ≫ s.π

Tactic:
simp only [biprod.inl_desc_assoc]

Goal state after:
case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inl ≫ s.π
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

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
K L : CochainComplex C ℤ
n m✝ p : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
β : Cochain K L m
hβ : δ m n β = ↑α
⊢ -α ∈ {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, δ m n β = ↑α}

Tactic:
exact ⟨m, hm, -β, by aesop⟩

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

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
K L : CochainComplex C ℤ
n m✝ p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property✝ : δ m n β ∈ cocycle K L n
⊢ Cochain.ofHom (Cocycle.rightShift ⟨δ m n β, property✝⟩ n 0 ⋯).homOf =
    δ (-1) 0 (n.negOnePow • β.rightShift n (-1) (CochainComplex.HomComplex.CohomologyClass.toHom._proof_4 n m hm)) +
      Cochain.ofHom 0

Tactic:
by simp [Cochain.δ_rightShift _ _ _ _ _ _ (zero_add n), smul_smul]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} C₂₃
inst✝¹⁷ : HasZeroMorphisms C₁
inst✝¹⁶ : HasZeroMorphisms C₂
inst✝¹⁵ : HasZeroMorphisms C₃
inst✝¹⁴ : Preadditive C₂₃
inst✝¹³ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁸ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : ¬c₁.π c₂₃ c₄ (c₁.next i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = j'
⊢ c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) ≠ j'

Tactic:
simpa only [← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄] using! h₂

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
⊢ (fun X ↦ ∃ K x, K.IsStrictlyGE 1) ≤ fun X ↦ ∃ K x, K.IsStrictlyGE 0

Tactic:
by
    rintro X ⟨K, e, _⟩
    exact ⟨K, e, K.isStrictlyGE_of_ge 0 1 (by lia)⟩

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

Goal state before:
pp: 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
⊢ Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
let o := Triangulated.someOctahedron' (by aesop) ((mem_distTriang_op_iff _).mp h₂₃)
      ((mem_distTriang_op_iff _).mp h₁₂) ((mem_distTriang_op_iff _).mp h₁₃)

Goal state after:
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' ⋯ ⋯ ⋯ ⋯
⊢ Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
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:
rw [← isLE_ι_obj_iff]
  change DerivedCategory.TStructure.t.IsLE ((DerivedCategory.singleFunctor C n).obj X) n
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
k : ℕ
hk :
  ∀ ⦃i j : ℕ⦄ (hk : j = i + k),
    F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk)) ≫ app j =
      app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk))
i j : ℕ
hk' : j = i + (k + 1)
⊢ F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j (k + 1) hk')) ≫ app j =
    app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j (k + 1) hk'))

Tactic:
obtain rfl : j = i + k + 1 := by lia

Goal state after:
case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
k : ℕ
hk :
  ∀ ⦃i j : ℕ⦄ (hk : j = i + k),
    F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk)) ≫ app j =
      app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk))
i : ℕ
hk' : i + k + 1 = i + (k + 1)
⊢ F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i (i + k + 1) (k + 1) hk')) ≫ app (i + k + 1) =
    app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i (i + k + 1) (k + 1) hk'))
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Injective fun f ↦ f.postcomp g

Tactic:
intro f₀

Goal state after:
case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ : LeftHomotopyClass X Y
⊢ ∀ ⦃a₂ : LeftHomotopyClass X Y⦄, (fun f ↦ f.postcomp g) f₀ = (fun f ↦ f.postcomp g) a₂ → f₀ = a₂
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
this : coprod.inr ≫ P.i ≫ sq.lift = coprod.inr ≫ coprod.desc f₀ f₁
⊢ P.i₁ ≫ sq.lift = f₁

Tactic:
rwa [P.inr_i_assoc, coprod.inr_desc] at this

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ Function.Injective fun g ↦ g.precomp f

Tactic:
intro f₀

Goal state after:
case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ : RightHomotopyClass Y Z
⊢ ∀ ⦃a₂ : RightHomotopyClass Y Z⦄, (fun g ↦ g.precomp f) f₀ = (fun g ↦ g.precomp f) a₂ → f₀ = a₂
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : FibrantObject C
⊢ WeakEquivalence (HoCat.ιCompResolutionNatTrans.app X)

Tactic:
by
  dsimp
  rw [weakEquivalence_toHoCat_map_iff, weakEquivalence_iff_of_objectProperty]
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
    CategoryTheory.Quotient.natIsoLift _
      (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator _ _ _)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lfibπ F)
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
have := Localization.essSurj L₂ W₂
    have L : Φ.LeftResolution (L₂.objPreimage X₂) := Classical.arbitrary _
    exact ⟨L.X₁, ⟨Localization.isoOfHom L₂ W₂ _ L.hw ≪≫ L₂.objObjPreimageIso X₂⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
⊢ W.Q.HasLeftKanExtension F ↔ L.HasLeftKanExtension F

Tactic:
hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F

Goal state after:
C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
⊢ W.Q.HasLeftKanExtension F ↔ W.Q.HasLeftKanExtension F
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
X : C₁
e : W₂.Q.obj (Φ.functor.obj X) ≅ (Φ.localizedFunctor W₁.Q W₂.Q).obj (W₁.Q.obj X) :=
  (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).app X
⊢ W₁.Q.HasPointwiseLeftKanExtensionAt (Φ.functor ⋙ F) (W₁.Q.obj X) ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.functor.obj X))

Tactic:
TwoSquare.hasPointwiseLeftKanExtensionAt_iff ((Φ.catCommSq W₁.Q W₂.Q).iso).hom,

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
X : C₁
e : W₂.Q.obj (Φ.functor.obj X) ≅ (Φ.localizedFunctor W₁.Q W₂.Q).obj (W₁.Q.obj X) :=
  (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).app X
⊢ W₂.Q.HasPointwiseLeftKanExtensionAt F ((Φ.localizedFunctor W₁.Q W₂.Q).obj (W₁.Q.obj X)) ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.functor.obj X))
Module: Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (isInjective C).limitsOfShape (Discrete J) ≤ isInjective C

Tactic:
by
    rintro Y ⟨p⟩
    have (j : J) : Injective (p.diag.obj ⟨j⟩) := p.prop_diag_obj _
    exact ⟨fun q i _ ↦ ⟨p.isLimit.lift (Cone.mk _
      (Discrete.natTrans (fun ⟨j⟩ ↦ (Injective.factorThru (q ≫ p.π.app ⟨j⟩) i :)))),
        p.isLimit.hom_ext (fun ⟨j⟩ ↦ by simp [p.isLimit.fac])⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
X : C
⊢ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)

Tactic:
exact (isPointwiseLeftKanExtensionOfIsoOfIsLocalization W
    (Localization.fac F hF W.Q).symm).hasPointwiseLeftKanExtension _

Goal state after: