mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : CategoryWithWeakEquivalences C
P : PathObject Y
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h : P.RightHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
induction h

Goal state after:
case mk
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : CategoryWithWeakEquivalences C
P : PathObject Y
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h✝ : X ⟶ P.P
h₀✝ : h✝ ≫ P.p₀ = f₀
h₁✝ : h✝ ≫ P.p₁ = f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, 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
a : A
⊢ lift.shiftIso hΦ 0 a a ⋯ = (Φ a).isoWhiskerLeft (shiftFunctorZero D A)

Tactic:
ext X
    apply G.map_injective
    simp [lift.map_shiftIso_hom_app, Functor.commShiftIso_zero]

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
inst✝¹ : IsTriangulated C
X : C
a b : ℤ
inst✝ : t.IsGE X a
⊢ t.IsGE ((t.truncLE b).obj X) a

Tactic:
dsimp [truncLE]; infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
φ' : (A.ι ⋙ L₂).obj X₁ ⟶ (A.ι ⋙ L₂).obj X₂
hφ' : φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂
f : B.trW.LeftFraction (A.ι.obj X₁) (A.ι.obj X₂)
hf : φ' = f.map L₂ ⋯
X₃ : C
s' : A.ι.obj X₂ ⟶ X₃
a : f.Y' ⟶ X₃
hX₃ : A X₃
hs' : (A ⊓ B).trW s'
fac : f.s ≫ a = s'
⊢ (B.inverseImage A.ι).trW (homMk s')

Tactic:
rwa [trW_inverseImage_ι_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ biprod.inr ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = biprod.inr ≫ 0

Tactic:
· simp [reassoc_of% σ₁.s_g, w₂]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝² : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝¹ : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝ : L₁.Additive
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ { obj := X₄, property := hX₄ } := homMk t
⊢ (B.inverseImage A.ι).trW t'

Tactic:
rwa [trW_inverseImage_ι_iff]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝ : Epi π
this : Mono ι
n : ℤ
⊢ (δ 1 2 (cochain₁ sq hsq hQ hK)).v n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯

Tactic:
have := Cochain.congr_v ((cocycle₁' sq hsq).δ_eq_zero 2) n _ rfl

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this : (δ 1 2 ↑(cocycle₁' sq hsq)).v n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯
⊢ (δ 1 2 (cochain₁ sq hsq hQ hK)).v n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.Quotient

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
x✝ : W.quotient homRel ((Quotient.functor homRel).map f)
f' : ((Quotient.functor homRel).1 X).as ⟶ ((Quotient.functor homRel).1 Y).as
hf' : W f'
h : (Quotient.functor homRel).map f = (Quotient.functor homRel).map f'
⊢ W f

Tactic:
← Functor.homRel_iff,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
x✝ : W.quotient homRel ((Quotient.functor homRel).map f)
f' : ((Quotient.functor homRel).1 X).as ⟶ ((Quotient.functor homRel).1 Y).as
hf' : W f'
h : (Quotient.functor homRel).homRel f f'
⊢ W f
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✝³ : IsFibrant Z
f : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsCofibrant Y
inst✝ : WeakEquivalence f
⊢ Function.Bijective fun g ↦ g.precomp f

Tactic:
by
  let h : CofibrantBrownFactorization f := Classical.arbitrary _
  have hj : Function.Bijective (fun (g : RightHomotopyClass Y Z) ↦ g.precomp h.p) := by
    rw [← Function.Bijective.of_comp_iff'
      (precomp_bijective_of_cofibration_of_weakEquivalence Z h.s)]
    convert! Function.bijective_id
    ext φ
    obtain ⟨φ, rfl⟩ := φ.mk_surjective
    simp
  convert! (precomp_bijective_of_cofibration_of_weakEquivalence Z h.i).comp hj using 1
  ext φ
  obtain ⟨φ, rfl⟩ := φ.mk_surjective
  simp

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 : C
inst✝⁴ : IsCofibrant X
inst✝³ : IsCofibrant Y
inst✝² : IsFibrant X
inst✝¹ : IsFibrant Y
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ ∃ g, RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
obtain ⟨g, hg⟩ := (precomp_bijective_of_weakEquivalence X f).2 (.mk (𝟙 X))
  obtain ⟨g, rfl⟩ := g.mk_surjective
  dsimp at hg
  refine ⟨g, by rwa [← mk_eq_mk_iff], ?_⟩
  rw [← mk_eq_mk_iff]
  apply (precomp_bijective_of_weakEquivalence Y f).1
  simp only [precomp_mk, Category.comp_id]
  rw [mk_eq_mk_iff, ← leftHomotopyRel_iff_rightHomotopyRel] at hg ⊢
  simpa using hg.postcomp f

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
⊢ Mono (homologyMap (ι f n₁) n₁)

Tactic:
by
  let n₀ := n₁ - 1
  rw [mono_homologyMap_iff_up_to_refinements _ n₀ n₁ (n₁ + 1) (by simp; lia) (by simp)]
  intro A x₁ _ y₀ hy₀
  obtain ⟨y₀, rfl⟩ : ∃ (z₁ : A ⟶ L.X n₀), z₁ ≫ (σ K L n₁).f n₀ = y₀ := by
    refine ⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩
    have : (biprod.inl : _ ⟶ mid K L n₁).f n₀ = 0 :=
      (isZero_single_obj_X (.up ℤ) _ _ _ (by lia)).eq_of_src _ _
    simp [this, ← biprod_total_f]
  simp only [Category.assoc, Hom.comm, biprodX_ext_to_iff, biprod_lift_fst_f,
    biprod_inr_fst_f, comp_zero, biprod_lift_snd_f, biprod_inr_snd_f,
    Category.comp_id] at hy₀
  obtain ⟨h₁, h₂⟩ := hy₀
  replace h₁ : x₁ ≫ K.pOpcycles n₁ = 0 := by
    rw [← cancel_mono (Injective.ι _)]
    simpa [i, ← cancel_mono (singleObjXSelf (.up ℤ) n₁ _).hom] using h₁
  obtain ⟨A₁, π, _, x₀, hx₀⟩ :=
    (K.comp_pOpcycles_eq_zero_iff_up_to_refinements x₁ n₀ (by simp; lia)).1 h₁
  exact ⟨A₁, π, inferInstance, x₀, hx₀⟩

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
X Y : FibrantObject C
inst✝ : IsCofibrant X.obj
f g : X ⟶ Y
⊢ (Quotient.functor (homRel C)).map f = (Quotient.functor (homRel C)).map g ↔ homRel C f g

Tactic:
← Functor.homRel_iff,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : FibrantObject C
inst✝ : IsCofibrant X.obj
f g : X ⟶ Y
⊢ (Quotient.functor (homRel C)).homRel f g ↔ homRel C f g
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
X₂ : D₂
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
have := Localization.essSurj L₂ W₂

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
X₂ : D₂
this : L₂.EssSurj
⊢ (Φ.functor ⋙ L₂).essImage X₂
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
have := Localization.essSurj L₂ W₂

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
this : L₂.EssSurj
⊢ (Φ.functor ⋙ L₂).essImage X₂
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
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} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
hw : w.GuitartExact
hw' : w'.GuitartExact
⊢ (w ≫ᵥ w').GuitartExact

Tactic:
simp only [TwoSquare.guitartExact_iff_initial]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
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} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : C₂ ⥤ C₃
R₂ : D₂ ⥤ D₃
H₃ : C₃ ⥤ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
hw : w.GuitartExact
hw' : w'.GuitartExact
⊢ ∀ (X₂ : D₁), ((w ≫ᵥ w').structuredArrowDownwards X₂).Initial
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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
⊢ Φ.IsRightDerivabilityStructure ↔ Φ.op.IsLeftDerivabilityStructure

Tactic:
refine ⟨fun ⟨_, _⟩ ↦ ?_, fun _ ↦ ?_⟩

Goal state after:
case refine_1
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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
x✝ : Φ.IsRightDerivabilityStructure
hasRightResolutions✝ : Φ.HasRightResolutions
guitartExact'✝ : TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
⊢ Φ.op.IsLeftDerivabilityStructure

case refine_2
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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
x✝ : Φ.op.IsLeftDerivabilityStructure
⊢ Φ.IsRightDerivabilityStructure
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
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := ⋯
⊢ ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ W.Q.map f))

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
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := ⋯
⊢ ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))

Tactic:
· intro Y₁ Y₂ f φ hφ
    convert! hP₁ f (homEquiv W W.Q L φ) hφ
    simp [homEquiv_comp]

Goal state after:
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
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := ⋯
⊢ ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0

Tactic:
rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : L.Acyclic
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ∃ i, e.f i = i'
⊢ IsZero ((K.stupidTrunc e).X i')

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ i, e.f i = i'
⊢ IsZero ((K.stupidTrunc e).X i')

Tactic:
· obtain ⟨i, hi⟩ := hi''
      exact (K.isZero_X_of_isStrictlySupported e' i' hi').of_iso (K.stupidTruncXIso e hi)

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ i, e.f i = i'
⊢ IsZero ((K.stupidTrunc e).X i')
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
⊢ IsZero ((K.stupidTrunc e).X i')

Tactic:
by
    by_cases hi'' : ∃ i, e.f i = i'
    · obtain ⟨i, hi⟩ := hi''
      exact (K.isZero_X_of_isStrictlySupported e' i' hi').of_iso (K.stupidTruncXIso e hi)
    · apply isZero_stupidTrunc_X
      simpa using hi''

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
⊢ ∀ {i j : ℤ}, (down ℤ).Rel i j → j.negOnePow = -i.negOnePow

Tactic:
rintro _ _ rfl; simp [Int.negOnePow_succ]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
⊢ ∃ f, ∃ (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α

Tactic:
have hα := α.δ_eq_zero (n + 1)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : δ n (n + 1) ↑α = 0
⊢ ∃ f, ∃ (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ f ≫ K.d q q' = 0

Tactic:
simpa using hα

Goal state after:
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 G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
have h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p := by simp

Goal state after:
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 G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ (ofComplex Z).d 1 0 = d (Projective.π Z)

Tactic:
simp [ofComplex]

Goal state after: