mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
⊢ i ≠ j → (fun i j ↦ v i / v j ∉ range v) i j

Tactic:
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.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hy : f a * ↑y = f x
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
⊢ y ∈ f.valueGroup

Tactic:
rw_mod_cast [hv₀, ha₀, Eq.comm, ← inv_mul_eq_iff_eq_mul] at hy

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ y ∈ f.valueGroup
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ (Units.mk0 (f r₁) hr₁)⁻¹ * Units.mk0 (f s₁) hs₁ = (Units.mk0 (f r₂) hr₂)⁻¹ * Units.mk0 (f s₂) hs₂ ↔
    f r₁ * f s₂ = f r₂ * f s₁

Tactic:
inv_mul_eq_inv_mul_iff_mul_eq_mul,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ Units.mk0 (f s₁) hs₁ * Units.mk0 (f r₂) hr₂ = Units.mk0 (f s₂) hs₂ * Units.mk0 (f r₁) hr₁ ↔ f r₁ * f s₂ = f r₂ * f s₁
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
h : ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
  use Y, i ≫ φ.hom, φ.inv ≫ e
  grind

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ P.p ≫ P.p ≫ P.p = P.p

Tactic:
repeat' rw [P.idem]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_map
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ autoParam
    (∀ (X Y : SimplicialObject C) (f : X ⟶ Y),
      (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
        eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

pp: case h_obj
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : SimplicialObject C),
    (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X

Tactic:
· intro X Y f
    ext n
    simp only [Functor.comp_map, HomologicalComplex.comp_f, alternatingFaceMapComplex_map_f,
      Functor.mapHomologicalComplex_map_f, HomologicalComplex.eqToHom_f, eqToHom_refl, comp_id,
      id_comp, SimplicialObject.whiskering_obj_map_app]

Goal state after:
case h_obj
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : SimplicialObject C),
    (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «1»
n : ℕ
i : Fin n
⊢ ↑(i.succ.castSucc.succAbove i.succ) = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Tactic:
rw [Fin.succAbove_castSucc_self]

Goal state after:
case «1»
n : ℕ
i : Fin n
⊢ ↑i.succ.succ = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)
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✝
n✝ : SimplexCategory
⊢ F.map η.left ≫ F.map (Y✝.hom.app n✝) = F.map (X✝.hom.app n✝) ≫ F.map (η.right.app n✝)

Tactic:
← F.map_comp,

Goal state after:
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✝
n✝ : SimplexCategory
⊢ F.map (η.left ≫ Y✝.hom.app n✝) = F.map (X✝.hom.app n✝) ≫ F.map (η.right.app n✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
      (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
⊢ False

Tactic:
apply not_le.mpr h'

Goal state after:
case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
      (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
⊢ y₂ ≤ y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Op

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
x : X.op _⦋n + 1⦌
⊢ (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.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
⊢ ⊤ ≤ ⨆ s, s.subcomplex

Tactic:
by
    rw [← Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top X, iSup_le_iff]
    rintro ⟨d, s, hs⟩
    exact le_trans (by rfl) (le_iSup _ (N.mk _ hs))

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
A : X.Subcomplex
d : ℕ
h✝ : X.HasDimensionLT d
⊢ A.toSSet.Finite

Tactic:
refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)

Goal state after:
X : SSet
inst✝ : X.Finite
A : X.Subcomplex
d : ℕ
h✝ : X.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite ↑(A.toSSet.nonDegenerate i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
A : X.Subcomplex
⊢ A.toSSet.Finite

Tactic:
obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite
  refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)
  apply Finite.of_injective (f := fun a ↦ a.1.1)
  rintro ⟨⟨x, _⟩, _⟩ ⟨⟨y, _⟩, _⟩ rfl
  rfl

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

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
⊢ Y.Finite

Tactic:
refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)

Goal state after:
X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite ↑(Y.nonDegenerate i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
simp [← A.mem_degenerate_iff ⟨x, hx⟩, h, Set.top_eq_univ, Set.mem_univ]

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

Goal state before:
pp: case pos
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
⊢ s.obj (i.castSucc.succAbove (i.predAbove j.succ)) = s.obj j.succ

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
        Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]

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

Goal state before:
pp: n i : ℕ
x✝¹ x✝ : Δ[n] _⦋i⦌
h : (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝¹ = (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝
⊢ objEquiv x✝¹ = objEquiv x✝

Tactic:
ext : 3; apply congr_fun h

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

Goal state before:
pp: case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : SimplexCategory
x : Δ[n].obj (op k)
hx : x ∈ (face S).obj (op k)
⊢ x ∈
    (Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))).obj (op k)

Tactic:
induction k using SimplexCategory.rec with | _ k

Goal state after:
case a.mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : x ∈ (face S).obj (op ⦋k⦌)
⊢ x ∈
    (Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
⊢ (stdSimplex.obj n).Finite

Tactic:
by
  induction n using SimplexCategory.rec with | _ n
  exact finite_of_hasDimensionLT _ (n + 1) inferInstance

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ↑({ toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨x, ⋯⟩) = ↑⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩

Tactic:
rw [← yonedaEquiv.right_inv x]

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ↑({ toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨yonedaEquiv.toFun (yonedaEquiv.invFun x), ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (X.map u)) (yonedaEquiv.toFun (yonedaEquiv.invFun x)), ⋯⟩
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:
d₂_eq' K c₁₂ i₁ h i₁₂,

Goal state after:
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₁₂
⊢ c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ 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'
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
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₁₂
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
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
A : C₄
f g : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
    ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ f = g

Tactic:
apply Cofan.IsColimit.hom_ext (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
  rintro ⟨i, hi⟩
  exact h _ _ _ hi

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

Goal state before:
pp: case neg
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₁
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
          (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c (c₁.prev i₁) i₂ j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
· rw [HomologicalComplex₂.d₂_eq_zero _ _ _ _ _ h₄, comp_zero, comp_zero, smul_zero,
          HomologicalComplex₂.d₂_eq_zero _ _ _ _ _ h₄, zero_comp, neg_zero]

Goal state after:
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 : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ ((p + 1) * y).negOnePow • (K.d p (p + 1)).f (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯ =
    (y + p * y).negOnePow • (K.d p (p + 1)).f (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯

Tactic:
congr 2

Goal state after:
case pos.e_a
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 : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (p + 1) * y = y + p * y
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 : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (p + y + p * y).negOnePow • (K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯ =
    (y + p * y + p).negOnePow • (K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯

Tactic:
congr 2

Goal state after:
case pos.e_a
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 : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + y + p * y = y + p * y + p
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 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

Tactic:
subst hp hq

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)
n p q : ℤ
⊢ h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p q ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : x ∈ coboundaries K L n
⊢ toHom (mk x) = 0

Tactic:
rw [← mk_eq_zero_iff] at h
    rw [h, map_zero]

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

Goal state before:
pp: 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
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : P.rightOrthogonal T.obj₁
h₃ : P.rightOrthogonal T.obj₃
X : C
f : X ⟶ T.obj₂
hX : P X
⊢ f = 0

Tactic:
by
    obtain ⟨g, rfl⟩ := Pretriangulated.Triangle.coyoneda_exact₂ T hT f (h₃ _ hX)
    simp [h₁ g hX]

Goal state after:
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 φ.s ≫ L.map α = L.map φ.f

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 φ.s ≫ L.map α = L.map ((fun g ↦ φ.s ≫ g) α)
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 α ≫ L.map φ.s = L.map φ.f

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 α ≫ L.map φ.s = L.map ((fun f ↦ f ≫ φ.s) α)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CategoryWithWeakEquivalences C
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst✝ : WeakEquivalence g
hfg : WeakEquivalence fg
⊢ WeakEquivalence f

Tactic:
subst fac
  exact weakEquivalence_of_postcomp f g

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
⊢ Fibration (P.trans P').p

Tactic:
let ψ : (P.trans P').P ⟶ P.P ⨯ A := prod.lift (pullback.fst _ _) (pullback.snd _ _ ≫ P'.p₁)
    rw [show (P.trans P').p = ψ ≫ prod.map P.p₀ (𝟙 A) by simp [PrepathObject.p, ψ]]
    have fac : ψ ≫ prod.map P.p₁ (𝟙 A) = pullback.snd _ _ ≫ P'.p := by
      ext
      · simp [ψ, pullback.condition]
      · simp [ψ]
    have sq : IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁ (P'.p ≫ prod.fst) := by
      simpa [ψ] using IsPullback.of_hasPullback P.p₁ P'.p₀
    have : Fibration ψ := by
      rw [fibration_iff]
      exact (fibrations C).of_isPullback
        (IsPullback.of_right sq fac (IsPullback.of_prod_fst_with_id P.p₁ A)).flip
          (by rw [← fibration_iff]; infer_instance)
    infer_instance

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₃ : Cᵒᵖ
⊢ ∀ {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:
Z₁₂

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₁₂ : Cᵒᵖ
⊢ ∀ {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₁₃)
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 ((quotient C (ComplexShape.up ℤ)).obj ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K))

Tactic:
plus_quotient_obj_iff

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
⊢ CochainComplex.plus C ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K)