mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ ∑ k ∈ range (n + 1), Δ_[1]^[n] ((n + 1).choose k • fun r ↦ r ^ k) = ↑(n + 1)!

Tactic:
fwdDiff_iter_const_smul,

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ (∑ x ∈ range (n + 1), (n + 1).choose x • Δ_[1]^[n] fun r ↦ r ^ x) = ↑(n + 1)!
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (∑ x ∈ range (P.natDegree + 1), Δ_[1]^[P.natDegree] (P.coeff x • fun i ↦ i ^ x)) x =
    (P.leadingCoeff • ↑P.natDegree !) x

Tactic:
fwdDiff_iter_const_smul,

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (∑ x ∈ range (P.natDegree + 1), P.coeff x • Δ_[1]^[P.natDegree] fun i ↦ i ^ x) x = (P.leadingCoeff • ↑P.natDegree !) x
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (fun a ↦ ∑ x ∈ range n, Δ_[1]^[n] (P x • fun i ↦ i ^ x) a) = 0

Tactic:
fwdDiff_iter_const_smul,

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (fun a ↦ ∑ x ∈ range n, (P x • Δ_[1]^[n] fun i ↦ i ^ x) a) = 0
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : SaturatedSubmonoid M
s₁ : Submonoid M
h₁ : s₁.MulSaturated
s₂ : Submonoid M
h₂ : s₂.MulSaturated
eq : { toSubmonoid := s₁, mulSaturated := h₁ }.toSubmonoid = { toSubmonoid := s₂, mulSaturated := h₂ }.toSubmonoid
⊢ { toSubmonoid := s₁, mulSaturated := h₁ } = { toSubmonoid := s₂, mulSaturated := h₂ }

Tactic:
by congr

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ p₁ = p₂

Tactic:
← cancel_epi f

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ f ≫ p₁ = f ≫ p₂
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ g.f = h.f

Tactic:
← cancel_epi f

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ f ≫ g.f = f ≫ h.f
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n m : ℕ
h : n = m
⊢ op ⦋n⦌ = op ⦋m⦌

Tactic:
by congr

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝³ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝² : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst✝¹ :
  ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst✝ :
  ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ (Truncated.cosk n).FullyFaithful

Tactic:
apply Adjunction.fullyFaithfulROfIsIsoCounit (coskAdj n)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
⊢ (const D).map (η.app (point.obj A)) ≫ ((whiskeringObj C D Y✝).obj A).hom =
    ((whiskeringObj C D X✝).obj A).hom ≫ (𝟭 (CosimplicialObject D)).map (whiskerLeft (drop.obj A) η)

Tactic:
ext n
            dsimp
            rw [Category.id_comp, Category.id_comp, η.naturality]

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.succAbove ⟨↑k + i, ⋯⟩) = ↑⟨↑k + (i + 1), ⋯⟩

Tactic:
Fin.succAbove_of_le_castSucc _ _ (by grind)

Goal state after:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑⟨↑k + i, ⋯⟩.succ = ↑⟨↑k + (i + 1), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case succ.succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : ↑j.succ = ↑j' + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
δ₀Iter_succ_assoc ..,

Goal state after:
case succ.succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : ↑j.succ = ↑j' + (i + 1)
⊢ δ₀Iter i ⋯ ≫ δ 0 ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'
Module: Mathlib.AlgebraicTopology.SimplicialSet.Op

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 1)
x : X.op _⦋n⦌
⊢ (ConcreteCategory.hom (SimplicialObject.σ X.op i)) x =
    opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.σ X i.rev)) (opObjEquiv x))

Tactic:
by
  simp [SimplicialObject.σ, op_map]

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

Goal state before:
pp: case succ
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n : ℕ
hi : n + (i + 1) = n + i + 1
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌

Tactic:
δ₀Iter_succ_assoc ..,

Goal state after:
case succ
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n : ℕ
hi : n + (i + 1) = n + i + 1
⊢ δ₀Iter i ⋯ ≫ δ 0 ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
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)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ (alternatingConst A hOdd hEven hc).iCycles j ≫ φ = 0

Tactic:
← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv

Goal state after:
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)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv ≫
      (alternatingConst A hOdd hEven hc).iCycles j ≫ φ =
    (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv ≫ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case a.mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), x i ∈ S
φ : Fin (k + 1) →o ↥S := { toFun := fun i ↦ ⟨x i, ⋯⟩, monotone' := ⋯ }
⊢ (ConcreteCategory.hom (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))))
      (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)) =
    x

Tactic:
ext j : 1

Goal state after:
case a.mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), x i ∈ S
φ : Fin (k + 1) →o ↥S := { toFun := fun i ↦ ⟨x i, ⋯⟩, monotone' := ⋯ }
j : Fin (k + 1)
⊢ ((ConcreteCategory.hom (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))))
        (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)))
      j =
    x j
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ Δ[n].nonDegenerate d ↔ Mono (objEquiv s)

Tactic:
mem_nonDegenerate_iff_strictMono,

Goal state after:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono ⇑s ↔ Mono (objEquiv s)
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₁₂
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₁₂' = 0

Tactic:
rw [K.d₁_eq_zero' c₁₂ h₁ i₂ i₁₂']

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₁₂
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₁₂ (c₁.next i₁, i₂) ≠ i₁₂'
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁶ : TotalComplexShape c₁ c₂ c
inst✝⁵ : TotalComplexShape c₂ c₁ c
inst✝⁴ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝³ : K.HasTotal c
inst✝² : DecidableEq J
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.flip.totalFlipIso c).hom.f j =
    K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j

Tactic:
ιTotal_totalFlipIso_f_hom

Goal state after:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁶ : TotalComplexShape c₁ c₂ c
inst✝⁵ : TotalComplexShape c₂ c₁ c
inst✝⁴ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝³ : K.HasTotal c
inst✝² : DecidableEq J
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ c₂.σ c₁ c i₂ i₁ • K.flip.ιTotal c i₂ i₁ j ⋯ = K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
⊢ ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
      ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
intro p q hpq

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
p q : ℤ
hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n₀
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
⊢ ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
      ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
intro p q hpq

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
p q : ℤ
hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n₀
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁')
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : (up ℤ).Rel n₀ n₁
⊢ ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        ((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        (y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
intro p q hpq

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : (up ℤ).Rel n₀ n₁
p q : ℤ
hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n₀
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : (up ℤ).Rel n₀ n₁
⊢ ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        ((shiftFunctor₂ C y).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        (y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
intro p q hpq

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : (up ℤ).Rel n₀ n₁
p q : ℤ
hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n₀
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₂ C y).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' 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:
· intro
    exact t.isGE_shift X n a n' hn'

Goal state after:
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 : HomotopyCategory C c
φ₁ φ₂ : K ⟶ L
hφ : (e.extendHomotopyFunctor C).map φ₁ = (e.extendHomotopyFunctor C).map φ₂
⊢ φ₁ = φ₂

Tactic:
by
    obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
    obtain ⟨L, rfl⟩ := HomotopyCategory.quotient_obj_surjective L
    obtain ⟨φ₁, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ₁
    obtain ⟨φ₂, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ₂
    exact HomotopyCategory.eq_of_homotopy _ _
      (.ofExtend (HomotopyCategory.homotopyOfEq _ _ hφ))

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.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:
· rintro ⟨K, e, _⟩ i hi
    apply ((K.exactAt_of_isLE n i hi).isZero_homology).of_iso
    exact (homologyFunctor C i).mapIso e ≪≫ (homologyFunctorFactors C i).app K

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.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ T.llp.IsStableUnderCoproductsOfShape J

Tactic:
by
  apply IsStableUnderCoproductsOfShape.mk
  intro A B _ _ f hf X Y p hp
  have := fun j ↦ hf j _ hp
  infer_instance

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

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

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_cylinder
  obtain ⟨Q, _⟩ := Cylinder.exists_very_good Z
  have sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i) := ⟨by aesop_cat⟩
  exact ⟨Q,
   ⟨{ h := sq.lift ≫ h.h
      h₀ := by
        have := coprod.inl ≫= sq.fac_left
        simp only [Q.inl_i_assoc, coprod.inl_desc] at this
        simp [reassoc_of% this]
      h₁ := by
        have := coprod.inr ≫= sq.fac_left
        simp only [Q.inr_i_assoc, coprod.inr_desc] at this
        simp [reassoc_of% this] }⟩⟩

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

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
P : ObjectProperty C
inst✝ : P.IsTriangulated
X Y : C
f : X ⟶ Y
Z : Cᵒᵖ
a : Opposite.op X ⟶ Z
b : Z ⟶ (shiftFunctor Cᵒᵖ 1).obj (Opposite.op Y)
h₁ : Triangle.mk f.op a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.op Z
⊢ P.trW f

Tactic:
rw [ObjectProperty.trW_iff']

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
P : ObjectProperty C
inst✝ : P.IsTriangulated
X Y : C
f : X ⟶ Y
Z : Cᵒᵖ
a : Opposite.op X ⟶ Z
b : Z ⟶ (shiftFunctor Cᵒᵖ 1).obj (Opposite.op Y)
h₁ : Triangle.mk f.op a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.op Z
⊢ ∃ X_1 f_1 h, ∃ (_ : Triangle.mk f_1 f h ∈ Pretriangulated.distinguishedTriangles), P X_1
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

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
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj (Opposite.unop Y)
h₁ : Triangle.mk f.unop a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.unop Z
⊢ P.trW f

Tactic:
rw [ObjectProperty.trW_iff']

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
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj (Opposite.unop Y)
h₁ : Triangle.mk f.unop a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.unop Z
⊢ ∃ X_1 f_1 h, ∃ (_ : Triangle.mk f_1 f h ∈ Pretriangulated.distinguishedTriangles), P X_1
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:
v₁₃

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),
    Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)