mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ zmultiples a ⊔ zmultiples b = closure {a, b}

Tactic:
zmultiples_eq_closure,

Goal state after:
a b : ℤ
⊢ closure {a} ⊔ closure {b} = closure {a, b}
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
⊢ τ a f = DomAddAct.mk (-a) +ᵥ f

Tactic:
by
  ext; simp [DomAddAct.vadd_apply, sub_eq_neg_add]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ (∃ y, x * y ∈ s) ↔ ∃ y, y * x ∈ s

Tactic:
mul_comm x

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
⊢ s.Pairwise fun i j ↦ v i / v j ∉ range v

Tactic:
intro i hi j hj hne

Goal state after:
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
⊢ v i / v j ∉ range v
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ p = equalizer.ι (𝟙 X) p

Tactic:
rw [← equalizer.condition, comp_id]

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

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
by
    let I := of (Set.image f ⊤)
    let e : X ⟶ I := ofHom ⟨fun x => ⟨f x, ⟨x, by tauto⟩⟩, fun x₁ x₂ h => f.hom.hom.monotone h⟩
    let m : I ⟶ Y := ofHom ⟨fun y => y.1, by tauto⟩
    have : Epi e := by
      rw [epi_iff_surjective]
      rintro ⟨_, y, h, rfl⟩
      exact ⟨y, rfl⟩
    have : StrongEpi e := strongEpi_of_epi e
    have : Mono m := ConcreteCategory.mono_of_injective _ (fun x y h => Subtype.ext h)
    exact ⟨⟨I, m, e, rfl⟩⟩

Goal state after:
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 : P ⟶ Q
⊢ f + 0 = f

Tactic:
ext
    apply add_zero

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'
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ Q.X.map φ

Tactic:
by
            rw [← Karoubi.comp_p_assoc]
            have h := hom_ext_iff.mp (f.naturality φ)
            dsimp [karoubiFunctorCategoryEmbedding] at h
            simp only [assoc, h.symm, karoubiFunctorCategoryEmbedding_obj,
              KaroubiFunctorCategoryEmbedding.obj_obj_p]
            rw [← P.p.naturality_assoc]
            exact congrArg _ (p_comp (f.app _)).symm

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_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (const D).map (F.map η.left) ≫
      { left := F.obj (point.obj Y✝), right := ((whiskering C D).obj F).obj (drop.obj Y✝),
          hom := (constComp SimplexCategory (point.obj Y✝) F).inv ≫ whiskerRight Y✝.hom F }.hom =
    { left := F.obj (point.obj X✝), right := ((whiskering C D).obj F).obj (drop.obj X✝),
          hom := (constComp SimplexCategory (point.obj X✝) F).inv ≫ whiskerRight X✝.hom F }.hom ≫
      (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F)

Tactic:
by
        ext
        dsimp
        rw [Category.id_comp, Category.id_comp, ← F.map_comp, ← F.map_comp]
        simp [w_app, map_comp]

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
⊢ (∃ x_1 ∈ A.obj x✝, (ConcreteCategory.hom (f.app x✝)) x_1 = x) → (ConcreteCategory.hom (inv (f.app x✝))) x ∈ A.obj x✝

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : X.obj x✝
hx : x ∈ A.obj x✝
⊢ (ConcreteCategory.hom (inv (f.app x✝))) ((ConcreteCategory.hom (f.app x✝)) x) ∈ A.obj x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
⊢ A.preimage (inv f) = A.image f

Tactic:
by
  ext _ x
  simp only [preimage_obj, NatIso.isIso_inv_app, Set.mem_preimage, image_obj, Set.mem_image]
  exact ⟨fun hx ↦ ⟨(inv f).app _ x, by simpa⟩, by rintro ⟨x, hx, rfl⟩; simpa⟩

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

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
this : IsSplitEpi f
⊢ y.simplex ∈ x.subcomplex.obj (Opposite.op ⦋y.dim⦌)

Tactic:
exact ⟨(section_ f).op, by simp [← hf, ← Functor.map_comp_apply, ← op_comp]⟩

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

Goal state before:
pp: case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this : IsSplitEpi f
⊢ (N.mk ↑y ⋯).simplex ∈
    { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex.obj (Opposite.op ⦋(N.mk ↑y ⋯).dim⦌)

Tactic:
have : Function.Injective (X.map f.op) := by
        rw [← mono_iff_injective]
        infer_instance

Goal state after:
case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this✝ : IsSplitEpi f
this : Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))
⊢ (N.mk ↑y ⋯).simplex ∈
    { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex.obj (Opposite.op ⦋(N.mk ↑y ⋯).dim⦌)
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: case right
n : ℕ
i : Fin (n + 2)
⊢ Function.Surjective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩

Tactic:
rintro ⟨j, hj⟩
        simp only [mem_compl, mem_singleton] at hj
        obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i
        · exact ⟨j.pred hj, by simp⟩
        · exact ⟨i.predAbove j, by aesop⟩

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

Goal state before:
pp: n : ℕ
x : Δ[n] _⦋0⦌
⊢ (fun i ↦ const n i (op ⦋0⦌)) ((fun x ↦ x 0) x) = x

Tactic:
ext i : 1; fin_cases i; rfl

Goal state after:
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₁✝ i₁'✝ : I₂
i₂✝ i₂'✝ : I₁
h₂ : c₂.Rel i₁✝ i₁'✝
h₁ : c₁.Rel i₂✝ i₂'✝
⊢ ((match (i₁✝, i₂✝) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂)) *
      match (i₁✝, i₂'✝) with
      | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂)) =
    -((match (i₁✝, i₂✝) with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂)) *
        match (i₁'✝, i₂✝) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂))

Tactic:
ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂,

Goal state after:
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₁✝ i₁'✝ : I₂
i₂✝ i₂'✝ : I₁
h₂ : c₂.Rel i₁✝ i₁'✝
h₁ : c₁.Rel i₂✝ i₂'✝
⊢ ((match (i₁✝, i₂✝) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂)) *
      match (i₁✝, i₂'✝) with
      | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂)) =
    -(-c₁.ε₁ c₂ c₁₂ (i₂✝, i₁✝) * c₁.ε₂ c₂ c₁₂ (i₂'✝, i₁✝))
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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h'

Tactic:
rw [d₂_eq' K c₁₂ i₁ h i₁₂, K.toGradedObject.ιMapObjOrZero_eq]

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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
⊢ f = g

Tactic:
by
  apply GradedObject.mapObj_ext
  rintro ⟨i₁, i₂⟩ hi
  exact h i₁ i₂ hi

Goal state after:
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 D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₂
⊢ CommShift (flipApp (𝟙 G₁) x✝) M

Tactic:
by
    simp only [flipApp, flipFunctor_obj, Functor.map_id, id_app]
    infer_instance

Goal state after:
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 D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₂
⊢ CommShift (flipApp (τ ≫ τ') x✝) M

Tactic:
by
    simp only [flipApp, flipFunctor_obj, Functor.map_comp, comp_app]
    infer_instance

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : 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 ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) •
      (G.map ((F₁₂.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂))).app (K₃.X i₃) ≫
        ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ (c₁.next i₁) i₂ i₃ j =
    0

Tactic:
rw [shape _ _ _ h, Functor.map_zero, zero_app, Functor.map_zero, zero_app, zero_comp, smul_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
n : ℤ
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
⊢ (f.f n).op =
    ((((dNext n) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
          (prevD n) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
        g.f n).op

Tactic:
obtain ⟨n, rfl⟩ : ∃ (m : ℤ), n = -m := ⟨-n , by simp⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
⊢ (f.f (-n)).op =
    ((((dNext (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
          (prevD (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
        g.f (-n)).op
Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ∀ (a b : Cocycle K L n),
    a ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm a) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)

Tactic:
intro y₁

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ : Cocycle K L n
⊢ ∀ (b : Cocycle K L n),
    y₁ ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm y₁) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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

Tactic:
extend.hom_eq _ _ rfl rfl,

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
⊢ (K.extendXIso e ⋯).hom ≫ h.hom i j ≫ (L.extendXIso e ⋯).inv = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
⊢ f.f i =
    (((dNext i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) +
        (prevD i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) +
      g.f i

Tactic:
simp only [← cancel_mono (L.extendXIso e rfl).inv,
      ← cancel_epi (K.extendXIso e rfl).hom, this, Preadditive.add_comp,
      Preadditive.comp_add, add_left_inj]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
⊢ (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom =
    (K.extendXIso e ⋯).hom ≫
        ((dNext i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) ≫
          (L.extendXIso e ⋯).inv +
      (K.extendXIso e ⋯).hom ≫
        ((prevD i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) ≫
          (L.extendXIso e ⋯).inv
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos.h
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:
· rw [← h₂, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]
        rfl

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

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

Tactic:
apply (Cochain.rightShiftAddEquiv _ _ _ n 0 (by simp)).injective

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

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

Tactic:
exact hX i hi

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

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

Tactic:
exact hX i hi

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : IsCofibrant X
⊢ IsCofibrant Y

Tactic:
by
  rw [isCofibrant_iff] at hX ⊢
  rw [Subsingleton.elim (initial.to Y) (initial.to X ≫ i)]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration P.i₀

Tactic:
← P.inl_i

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration (coprod.inl ≫ P.i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
n : ℤ
K : CochainComplex C ℤ
q : ℤ
h✝ : K.IsStrictlyGE q
⊢ plus C ((shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj ((quotient C (ComplexShape.up ℤ)).obj K))

Tactic:
shift_quotient_obj,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
n : ℤ
K : CochainComplex C ℤ
q : ℤ
h✝ : K.IsStrictlyGE q
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K))
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
K L : HomotopyCategory.Plus C
x✝ : CochainComplex.IsKInjective L.obj.as
this : Function.Bijective DerivedCategory.Qh.map
⊢ Function.Bijective Qh.map

Tactic:
← Function.Bijective.of_comp_iff _
    ((HomotopyCategory.Plus.fullyFaithfulι C).map_bijective _ _)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : HomotopyCategory.Plus C
x✝ : CochainComplex.IsKInjective L.obj.as
this : Function.Bijective (DerivedCategory.Qh.map ∘ (HomotopyCategory.Plus.ι C).map)
⊢ Function.Bijective Qh.map