mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case inr
n : ℕ
k : Fin ⦋n + 1⦌.len
⊢ ↑((ConcreteCategory.hom (σ₀Iter 1 ⋯)) k.succ) = ↑((ConcreteCategory.hom (σ 0)) k.succ)

Tactic:
· rw [σ₀Iter_coe_eq_of_ge .., coe_σ]
    simp

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

Goal state before:
pp: n : ℕ
⊢ σ₀Iter 1 ⋯ = σ 0

Tactic:
by
  refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  dsimp
  obtain rfl | ⟨k, rfl⟩ := k.eq_zero_or_eq_succ
  · rw [σ₀Iter_coe_eq_of_lt _ _ _ (by simp), coe_σ,
      Fin.predAbove_of_le_castSucc _ _ (by simp)]
    dsimp
  · rw [σ₀Iter_coe_eq_of_ge .., coe_σ]
    simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
⊢ δ i ≫ σ₀Iter (j + 1) h = σ₀Iter j ⋯

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  dsimp
  rw [dsimp% ConcreteCategory.comp_apply (δ i) (σ₀Iter (j + 1))]
  by_cases! hk : j ≤ k.val
  · rw [σ₀Iter_coe_eq_of_ge j .., coe_δ]
    by_cases! hk' : i ≤ k.castSucc
    · rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_ge ..]
      simp
    · obtain rfl : j = k.val := by grind [dsimp% Fin.lt_def.1 hk']
      rw [Fin.succAbove_of_castSucc_lt _ _ (by lia),
        σ₀Iter_coe_eq_of_lt .., tsub_self]
  · rw [σ₀Iter_coe_eq_of_lt j .., coe_δ]
    by_cases! hk' : i ≤ k.castSucc
    · rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_lt ..]
    · rw [Fin.succAbove_of_castSucc_lt _ _ (by lia), σ₀Iter_coe_eq_of_lt ..]

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

Goal state before:
pp: S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ (ConcreteCategory.hom (SimplicialObject.σ S i ≫ f.app (op ⦋n + 1⦌))) x =
    (ConcreteCategory.hom (f.app (op ⦋n⦌) ≫ SimplicialObject.σ T i)) x

Tactic:
exact congr_hom (SimplicialObject.σ_naturality f i) x

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

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) →
    ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))

pp: case mpr
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))) →
    ∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
· obtain ⟨x, rfl⟩ := opObjEquiv.symm.surjective x
    rintro ⟨f, _, y, rfl⟩
    exact ⟨SimplexCategory.rev.map f, inferInstance, opObjEquiv.symm y, by simp [op_map]⟩

Goal state after:
case mpr
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))) →
    ∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

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

Tactic:
constructor
    · have := (mem_nonDegenerate_iff_mono x.val).1 x.property
      rw [SimplexCategory.mono_iff_injective] at this
      exact fun _ _ h ↦ this (by simpa using h)
    · rintro ⟨j, hj⟩
      rw [nonDegenerateEquiv'_iff] at hj
      aesop

Goal state after:
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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁₂ (i₁, i₂) •
        (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' ⋯) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0

Tactic:
simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]

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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0
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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ⋯) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0

Tactic:
simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]

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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.d₁ c₁₂ i₁ (c₂.next i₂) i₁₂'' = 0
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case neg
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₁
⊢ ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁'

Tactic:
rw [D₁_shape _ _ _ _ h, zero_comp, D₁_shape, comp_zero, smul_zero]

Goal state after:
case neg.h₁₂
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₁
⊢ ¬(up ℤ).Rel n₀' n₁'
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case neg
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₁
⊢ ((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁'

Tactic:
rw [D₁_shape _ _ _ _ h, zero_comp, D₁_shape, comp_zero, smul_zero]

Goal state after:
case neg.h₁₂
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₁
⊢ ¬(up ℤ).Rel n₀' n₁'
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
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
m : s.pt ⟶ sq.kernelFork.pt
hm : (m ≫ biprod.lift fst snd) ≫ biprod.snd = s.ι ≫ biprod.snd
⊢ m ≫ snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd

Tactic:
simp only [assoc, biprod.lift_snd] at hm

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
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
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ snd = s.ι ≫ biprod.snd
⊢ m ≫ snd = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ snd
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ t ≫ h.desc u ⋯.lift ⋯ ≫ g' = t ≫ v

Tactic:
rw [h.inr_desc_assoc, CommSq.fac_right]

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
⊢ WeakEquivalence (P.trans P'.toPrecylinder).π

Tactic:
by
    have : WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫
        pushout.desc P.π P'.π (by simp)) := by
      simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app,
        Precylinder.i₀_π]
      infer_instance
    dsimp
    apply weakEquivalence_of_precomp (P.i₀ ≫ pushout.inl _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

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
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
F : Quotient L.homRel ⥤ D := Quotient.lift L.homRel L ⋯
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
hf : W f
⊢ IsIso ((Quotient.functor L.homRel).map f)

Tactic:
have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf
    apply isIso_of_reflects_iso _ F

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

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
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
F : Quotient L.homRel ⥤ D := Quotient.lift L.homRel L ⋯
⊢ L.IsLocalization W

Tactic:
have hW' : W.IsInvertedBy (Quotient.functor L.homRel) := fun _ _ f hf ↦ by
    have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf
    apply isIso_of_reflects_iso _ F

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
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
F : Quotient L.homRel ⥤ D := Quotient.lift L.homRel L ⋯
hW' : W.IsInvertedBy (Quotient.functor L.homRel)
⊢ L.IsLocalization W
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p

Tactic:
have := sq.fac_right =≫ prod.snd
        simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this
        simp [this]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹³ : Category.{u_5, u_1} C
inst✝¹² : Category.{u_6, u_2} D
inst✝¹¹ : Category.{u_7, u_3} E
A : Type u_4
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝⁷ : G.CommShift A
inst✝⁶ : G.Full
inst✝⁵ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : G.Additive
a : A
inst✝ : (F.functor a).Additive
⊢ (Φ a ⋙ G).Additive

Tactic:
rwa [Functor.additive_iff_of_iso (hΦ a)]

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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsIso ((t.truncGTπ n₀).app X)

Tactic:
exact (MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (Arrow.isoMk (Iso.refl _) ((t.truncGTIsoTruncGE _ _ hn₁).symm.app X))

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
i : { obj := A, property := hA } ⟶ { obj := B, property := hB }
inst✝¹ : Mono i
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
t : { obj := A, property := hA } ⟶ { obj := X, property := hX }
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
b : { obj := B, property := hB } ⟶ { obj := Y, property := hY }
p : { obj := X, property := hX } ⟶ { obj := Y, property := hY }
inst✝ : Fibration p
hip : WeakEquivalence i ∨ WeakEquivalence p
sq : CommSq t i p b
hi : Mono i.hom
hp : degreewiseEpiWithInjectiveKernel p.hom
⊢ sq.HasLift

Tactic:
obtain ⟨i, rfl⟩ := ObjectProperty.homMk_surjective i

Goal state after:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
t : { obj := A, property := hA } ⟶ { obj := X, property := hX }
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
b : { obj := B, property := hB } ⟶ { obj := Y, property := hY }
p : { obj := X, property := hX } ⟶ { obj := Y, property := hY }
inst✝¹ : Fibration p
hp : degreewiseEpiWithInjectiveKernel p.hom
i : { obj := A, property := hA }.obj ⟶ { obj := B, property := hB }.obj
inst✝ : Mono (ObjectProperty.homMk i)
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence p
sq : CommSq t (ObjectProperty.homMk i) p b
hi : Mono (ObjectProperty.homMk i).hom
⊢ sq.HasLift
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
⊢ QuasiIsoAt (π K L n₁) i

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]
    have : homologyMap (biprod.inl : _ ⟶ mid K L n₁) i = 0 :=
      (ShortComplex.isZero_homology_of_isZero_X₂ _
        (isZero_single_obj_X (.up ℤ) _ _ _ (by lia))).eq_of_src _ _
    refine ⟨homologyMap (σ K L n₁) i, ?_, ?_⟩
    · simp [← homologyMap_id, ← biprod.total, homologyMap_comp, this]
    · simp [← homologyMap_comp, homologyMap_id]

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
⊢ QuasiIsoAt (ι f n₁) i

Tactic:
have := quasiIsoAt_π K L n₀ n₁ hn₁ i hi
  rw [← quasiIsoAt_iff_comp_right _ (π K L n₁), ι_π]
  exact hf i hi

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : RightHomotopyRel x✝¹ x✝
⊢ LeftHomotopyClass.mk x✝¹ = LeftHomotopyClass.mk x✝

Tactic:
rw [LeftHomotopyClass.mk_eq_mk_iff]
    exact h.leftHomotopyRel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (FibrantObject.HoCat C)).Q

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
⊢ (cokernel f).IsGE n

Tactic:
exact isGE_cokernel f n hf

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₃ X₃' : C₃
e : X₃ ≅ X₃'
⊢ (w.costructuredArrowRightwards X₃).Final ↔ (w.costructuredArrowRightwards X₃').Final

Tactic:
rw [Functor.final_iff_comp_equivalence _ (CostructuredArrow.mapIso (B.mapIso e)).functor,
    Functor.final_iff_equivalence_comp (CostructuredArrow.mapIso e).functor]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₃ X₃' : C₃
e : X₃ ≅ X₃'
⊢ (w.costructuredArrowRightwards X₃ ⋙ (CostructuredArrow.mapIso (B.mapIso e)).functor).Final ↔
    ((CostructuredArrow.mapIso e).functor ⋙ w.costructuredArrowRightwards X₃').Final
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
hw : w.GuitartExact
X₃ : C₃
⊢ (w.costructuredArrowRightwards X₃).Final

Tactic:
rw [guitartExact_iff_final] at hw

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
hw : ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
X₃ : C₃
⊢ (w.costructuredArrowRightwards X₃).Final
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q : ℕ
i : ℤ
⊢ (midπ f n₀ q).f i ≫ ((functor f n₀).obj (op q)).obj.π.f i = (π f n₀).f i

Tactic:
by
  rw [← midπ_π f n₀ q]
  dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
⊢ Φ.IsLeftDerivabilityStructure ↔ Φ.op.IsRightDerivabilityStructure

Tactic:
by
  let F := Φ.localizedFunctor W₁.Q W₂.Q
  let e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := (Φ.catCommSq W₁.Q W₂.Q).iso
  let e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
  have eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv :=
    TwoSquare.guitartExact_op_iff _
  constructor
  · rintro ⟨_, _⟩
    rwa [Φ.op.isRightDerivabilityStructure_iff _ _ _ e', eq]
  · intro
    have : Φ.HasLeftResolutions := by
      rw [hasLeftResolutions_iff_op]
      infer_instance
    refine ⟨inferInstance, ?_⟩
    rw [← eq]
    exact Φ.op.guitartExact_of_isRightDerivabilityStructure' _ _ _ e'

Goal state after:
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: case hP₁
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk g.hom.op
Y₁✝ Y₂✝ : Cᵒᵖ
f : Y₁✝ ⟶ Y₂✝
φ : L.op.obj (op Y) ⟶ L.op.obj Y₁✝
hφ : P (CostructuredArrow.mk (StructuredArrow.mk φ).hom.unop)
⊢ P (CostructuredArrow.mk (StructuredArrow.mk (φ ≫ L.op.map f)).hom.unop)

Tactic:
exact hP₁ f.unop φ.unop hφ

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ ExactAt P.complex (n + 1)

Tactic:
rw [← quasiIsoAt_iff_exactAt' P.π (n + 1) (exactAt_succ_single_obj _ _)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt P.π (n + 1)
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ ((F.map P.p).f ≫ (F.obj P.X).p) ≫ (F.map P.p).f = (F.map P.p).f

Tactic:
rw [comp_p, ← comp_f, ← F.map_comp, P.idem]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ Homotopy (lift (f ≫ g) P R) (lift f P Q ≫ lift g Q R)

Tactic:
by
  apply liftHomotopy (f ≫ g) <;> simp

Goal state after: