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

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = (-a).prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
Finsupp.prod_neg_index

Goal state after:
case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = a.prod fun a b ↦ f a ^ (-b)

case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∀ (a : ι), f a ^ 0 = 1
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: n : ℕ
⊢ (nsmulAddMonoidHom n).range = zmultiples ↑n

Tactic:
by
  ext m : 1
  simp [mem_zmultiples_iff, dvd_def]
  grind

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ y✝ : M
hx✝ : x✝ ∈ s.saturation
hy✝ : y✝ ∈ s.saturation
ih₁ : ∃ y, x✝ * y ∈ s
ih₂ : ∃ y, y✝ * y ∈ s
y₁ : M
h₁ : x✝ * y₁ ∈ s
y₂ : M
h₂ : y✝ * y₂ ∈ s
⊢ x✝ * y✝ * (y₁ * y₂) ∈ s

Tactic:
rw [mul_mul_mul_comm]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ y✝ : M
hx✝ : x✝ ∈ s.saturation
hy✝ : y✝ ∈ s.saturation
ih₁ : ∃ y, x✝ * y ∈ s
ih₂ : ∃ y, y✝ * y ∈ s
y₁ : M
h₁ : x✝ * y₁ ∈ s
y₂ : M
h₂ : y✝ * y₂ ∈ s
⊢ x✝ * y₁ * (y✝ * y₂) ∈ s
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rcases le_or_gt k (j.castSucc) with (hjk | hjk)

Goal state after:
case inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

case inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i ≤ (j.predAbove k).castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
have hjk := H.trans_lt' hik

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
rcases le_or_gt k (j.castSucc) with (hjk | hjk)

Goal state after:
case inl.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

case inl.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)

pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
· rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hik)]
    rcases le_or_gt k (j.castSucc) with (hjk | hjk)
    · rw [Fin.predAbove_of_le_castSucc _ _
      (Fin.castSucc_le_castSucc_iff.mpr hjk), Fin.castPred_castSucc,
      Fin.predAbove_of_le_castSucc _ _ hjk, Fin.succAbove_of_castSucc_lt, Fin.castSucc_castPred]
      rw [Fin.castSucc_castPred]
      exact hjk.trans_lt H
    · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hjk),
      Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_pred_eq_pred_castSucc]
      rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ ((-1) ^ 0 • X.left.δ 0 + (-1) ^ ↑1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
pow_zero,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (1 • X.left.δ 0 + (-1) ^ ↑1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).map f ≫
          (((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj Y)).symm
            ⟨Y.hom.app (op ⦋0⦌), ⋯⟩).f
      0 =
    ((((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj X)).symm
            ⟨X.hom.app (op ⦋0⦌), ⋯⟩ ≫
          (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C).map f).f
      0

Tactic:
#adaptation_note /-- This proof broke at nightly-2026-04-28. It used to be:
    ```
    dsimp
    simp [ChainComplex.toSingle₀Equiv, SimplicialObject.Augmented.w₀]
    ```
    The proof below is an emergency repair, and I've asked the authors of this file to review.
    -/

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).map f ≫
          (((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj Y)).symm
            ⟨Y.hom.app (op ⦋0⦌), ⋯⟩).f
      0 =
    ((((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj X)).symm
            ⟨X.hom.app (op ⦋0⦌), ⋯⟩ ≫
          (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C).map f).f
      0
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ 0 • X.δ 0) =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow

Tactic:
pow_zero,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ (1 • X.δ 0) =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + i = m
⊢ X.σ₀Iter (i + 1) ⋯ = X.σ₀Iter i h ≫ X.σ 0

Tactic:
simp [σ₀Iter, SimplexCategory.σ₀Iter_succ' _ h, σ_def]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    (cechNerveEquiv X' Y).symm (f ≫ g) = Augmented.toArrow.map f ≫ (cechNerveEquiv X Y).symm g

Tactic:
dsimp [cechNerveEquiv]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    equivalenceRightToLeft X' Y (f ≫ g) = Augmented.toArrow.map f ≫ equivalenceRightToLeft X Y g
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    (cechNerveEquiv X Y') (f ≫ g) = (cechNerveEquiv X Y) f ≫ augmentedCechNerve.map g

Tactic:
dsimp [cechNerveEquiv]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    { toFun := equivalenceLeftToRight X Y', invFun := equivalenceRightToLeft X Y', left_inv := ⋯, right_inv := ⋯ }
        (f ≫ g) =
      { toFun := equivalenceLeftToRight X Y, invFun := equivalenceRightToLeft X Y, left_inv := ⋯, right_inv := ⋯ } f ≫
        augmentedCechNerve.map g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.degenerate (n + 1) = ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

Tactic:
by
  ext x
  constructor
  · intro hx
    rw [mem_degenerate_iff] at hx
    obtain ⟨m, hm, f, hf, y, rfl⟩ := hx
    obtain ⟨i, θ, rfl⟩ := SimplexCategory.eq_σ_comp_of_not_injective f (fun hf ↦ by
      rw [← SimplexCategory.mono_iff_injective] at hf
      have := SimplexCategory.le_of_mono f
      lia)
    aesop
  · intro hx
    simp only [Set.mem_iUnion, Set.mem_range] at hx
    obtain ⟨i, y, rfl⟩ := hx
    apply σ_mem_degenerate

Goal state after:
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⟩

Goal state after:
case right
n : ℕ
i j : Fin (n + 2)
hj : j ∈ {i}ᶜ
⊢ ∃ a, (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ Δ[n].nonDegenerate d ↔ StrictMono ⇑s

Tactic:
rw [← nonDegenerate_iff_of_mono (isoNerve n).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_strictMono]

Goal state after:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono ((ConcreteCategory.hom ((isoNerve.{u} n).hom.app (op ⦋d⦌))) s).obj ↔ StrictMono ⇑s
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case left
n m : ℕ
x₁ : Δ[n] _⦋m⦌
h₁ : x₁ ∈ Δ[n].nonDegenerate m
x₂ : Δ[n] _⦋m⦌
h₂ : x₂ ∈ Δ[n].nonDegenerate m
h₃ :
  (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨x₁, h₁⟩ =
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨x₂, h₂⟩
⊢ ⟨x₁, h₁⟩ = ⟨x₂, h₂⟩

Tactic:
obtain ⟨f₁, rfl⟩ := objEquiv.symm.surjective x₁

Goal state after:
case left
n m : ℕ
x₂ : Δ[n] _⦋m⦌
h₂ : x₂ ∈ Δ[n].nonDegenerate m
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
h₃ :
  (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objEquiv.symm f₁, h₁⟩ =
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨x₂, h₂⟩
⊢ ⟨objEquiv.symm f₁, h₁⟩ = ⟨x₂, h₂⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Surjective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
rintro ⟨j, hj⟩

Goal state after:
case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
hj : j ∈ ↑(nonDegenerateEquiv' x)
⊢ ∃ a, (fun i ↦ ⟨↑x i, ⋯⟩) a = ⟨j, hj⟩
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
⊢ (↾fun x ↦ objMk ((OrderHom.const (Fin ((unop (op ⦋0⦌)).len + 1))) 0)) ≫ (stdSimplex.obj Δ).hom.app (op ⦋0⦌) =
    𝟙 (stdSimplex.obj Δ).right

Tactic:
by
    dsimp
    subsingleton

Goal state after:
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₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c.Rel j (c.next j)
⊢ c₁.ε₂ c₂ c (i₁, i₂) •
      (F.obj (K₁.X i₁)).map (K₂.d i₂ (c₂.next i₂)) ≫
        (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ (c₂.next i₂) (c.next j) ⋯ ≫
          hom₁ h₁ f₂ F c (c.next j) j =
    0

Tactic:
ιMapBifunctor_hom₁ _ _ _ _ _ _ _ _ _ _ rfl,

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₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c.Rel j (c.next j)
⊢ c₁.ε₂ c₂ c (i₁, i₂) •
      (F.obj (K₁.X i₁)).map (K₂.d i₂ (c₂.next i₂)) ≫
        (c₁.ε₁ c₂ c (c₁.prev i₁, c₂.next i₂) •
          (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X (c₂.next i₂)) ≫
            (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f (c₂.next i₂)) ≫
              L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) (c₂.next i₂) j) =
    0
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₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
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
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
⊢ hom₂ f₁ h₂ F c = H.hom

Tactic:
ext j j' i₁ i₂ hj
    dsimp [H, mapBifunctorMapHomotopy₁]
    rw [add_zero, zero_add, ι_mapBifunctorFlipIso_inv_assoc, Linear.units_smul_comp,
      ιMapBifunctor_hom₁_assoc h₂ f₁ F.flip c _ i₂ i₁ j j'
        (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, hj]) rfl,
      ιMapBifunctor_hom₂ f₁ h₂ F c i₁ _ i₂ j j' hj rfl]
    dsimp
    simp only [NatTrans.naturality_assoc, Linear.units_smul_comp, assoc]
    by_cases hj' : c₁.π c₂ c (i₁, c₂.prev i₂) = j'
    · rw [ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ hj',
        ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ (by rwa [ComplexShape.π_symm c₁ c₂ c]),
        ι_mapBifunctorFlipIso_hom, Linear.comp_units_smul, Linear.comp_units_smul,
        smul_smul, smul_smul]
      by_cases hi₂ : c₂.Rel (c₂.prev i₂) i₂
      · congr 1
        nth_rw 2 [mul_comm]
        rw [← ComplexShape.σ_ε₂ c₁ c i₁ hi₂, mul_comm, ← mul_assoc,
          Int.units_mul_self, one_mul]
      · rw [h₂.zero _ _ hi₂, Functor.map_zero, zero_comp, comp_zero, smul_zero, smul_zero]
    · rw [ιMapBifunctorOrZero_eq_zero _ _ _ _ _ _ _ hj',
        ιMapBifunctorOrZero_eq_zero _ _ _ _ _ _ _ (by rwa [ComplexShape.π_symm c₁ c₂ c]),
        comp_zero, comp_zero, smul_zero, zero_comp, comp_zero,
        comp_zero, smul_zero, smul_zero]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
x : ↑((forget₂ C Ab).obj (K.X i))
j : ι
hj : c.next i = j
hx : (ConcreteCategory.hom ((forget₂ C Ab).map (K.d i j))) x = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (K.iCycles i))) (K.cyclesMk x j hj hx) = x

Tactic:
subst hj
  apply (K.sc i).i_cyclesMk

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ biprod.fst ≫ f - s.ι ≫ biprod.snd ≫ g = 0

Tactic:
← Preadditive.comp_sub

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ (biprod.fst ≫ f - biprod.snd ≫ g) = 0
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P✝ : C
b : P✝ ⟶ ⋯.shortComplex'.X₁
hb : b ≫ ⋯.shortComplex'.f = 0
⊢ b = 0

Tactic:
exact Fork.IsLimit.hom_ext h.isLimitKernelFork (by simpa using hb)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℕ
inst✝¹ : ∀ (n : ℕ), Injective (K.X n)
inst✝ : ∀ (n : ℕ), Injective (L.X n)
f : K ⟶ L
⊢ QuasiIso (extendMap f ComplexShape.embeddingUpNat) ↔ homotopyEquivalences C (ComplexShape.up ℕ) f

Tactic:
CochainComplex.IsKInjective.quasiIso_iff,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℕ
inst✝¹ : ∀ (n : ℕ), Injective (K.X n)
inst✝ : ∀ (n : ℕ), Injective (L.X n)
f : K ⟶ L
⊢ homotopyEquivalences C (ComplexShape.up ℤ) (extendMap f ComplexShape.embeddingUpNat) ↔
    homotopyEquivalences C (ComplexShape.up ℕ) f
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

Tactic:
by
  rw [le_llp_iff_le_rlp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp

Tactic:
by
  intro A B i hi
  rw [coproducts_iff] at hi
  obtain ⟨J, hi⟩ := hi
  exact T.colimitsOfShape_discrete_le_llp_rlp J _ hi

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : (fibrations C).IsStableUnderBaseChange
hf : Fibration f
⊢ Fibration (pullback.snd f g)

Tactic:
by
  rw [fibration_iff] at hf ⊢
  exact MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g) hf

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (weakEquivalences C).ContainsIdentities
X : C
⊢ WeakEquivalence (𝟙 X)

Tactic:
rw [weakEquivalence_iff]
  apply id_mem

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
⊢ IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)

Tactic:
simpa [ψ] using IsPushout.of_hasPushout P.i₁ P'.i₀

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: 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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst✝ : t.IsLE Y n
this : t.IsLE Y (n + 1 - 1)
⊢ f₁ = f₂

Tactic:
rw [← cancel_mono ((t.truncLEIsoTruncLT n (n + 1) rfl).hom.app _)]

Goal state after:
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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst✝ : t.IsLE Y n
this : t.IsLE Y (n + 1 - 1)
⊢ f₁ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X = f₂ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

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

Tactic:
refine ⟨fun _ ↦ ?_,
    fun _ ↦ t.isLE_of_iso (asIso (((t.truncLTι (n₀ + 1))).app X)) n₀⟩

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ : ℤ
X : C
x✝ : t.IsLE X n₀
⊢ IsIso ((t.truncLTι (n₀ + 1)).app X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
a b : ℤ
inst✝ : t.IsLE X b
this : IsIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))
⊢ IsZero ((t.truncGE (b + 1)).obj ((𝟭 C).obj X))

Tactic:
rwa [← isLE_iff_isZero_truncGE_obj _ _ _ rfl]

Goal state after: