mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ofSimplex x).image f ≤ ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
rw [image_le_iff, ofSimplex_le_iff, preimage_obj, Set.mem_preimage]
    apply mem_ofSimplex_obj

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

Goal state before:
pp: X : SSet
x : X.S
⊢ ∃ x_1, x_1.subcomplex = x.subcomplex

Tactic:
obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
    obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x
    refine ⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩
    · simp only [Subcomplex.ofSimplex_le_iff]
      have := isSplitEpi_of_epi f
      have : Function.Injective (X.map f.op) := by
        rw [← mono_iff_injective]
        infer_instance
      refine ⟨(section_ f).op, this ?_⟩
      dsimp
      rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]
    · simp only [Subcomplex.ofSimplex_le_iff]
      exact ⟨f.op, rfl⟩

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

Goal state before:
pp: X : SSet
⊢ ⨆ x, ofSimplex ↑x.snd = ⊤

Tactic:
eq_top_iff_contains_nonDegenerate

Goal state after:
X : SSet
⊢ ∀ (n : ℕ), X.nonDegenerate n ⊆ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ l, ↑i = ↑j + 1 + l

Tactic:
rw [Fin.castSucc_lt_iff_succ_le, Fin.le_def] at hij
      obtain ⟨l, hl⟩ := Nat.le.dest hij
      exact ⟨l, by grind⟩

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
⊢ ∀ (p q : ℕ), (down ℕ).Rel p q → (MonoidHom.mk' (fun i ↦ (-1) ^ i) ⋯) q = -(MonoidHom.mk' (fun i ↦ (-1) ^ i) ⋯) p

Tactic:
by
    rintro _ q rfl
    dsimp
    rw [pow_add, pow_one, mul_neg, mul_one, neg_neg]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (K.X i)

Tactic:
rw [IsZero.iff_id_eq_zero]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ 𝟙 (K.X i) = 0
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (K.X i)

Tactic:
rw [IsZero.iff_id_eq_zero]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ 𝟙 (K.X i) = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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

Tactic:
simp only [extendMap_f _ _ rfl] at this

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

Goal state before:
pp: case mp
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
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE ((shiftFunctor C a).obj X) n' → t.IsGE X n

pp: case mpr
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
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE X n → t.IsGE ((shiftFunctor C a).obj X) n'

Tactic:
· intro
    exact t.isGE_of_shift X n a n' hn'

Goal state after:
case mpr
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
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE X n → t.IsGE ((shiftFunctor C a).obj X) n'
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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
X : C
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE X n₁
⊢ IsZero X

Tactic:
rw [IsZero.iff_id_eq_zero]

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
X : C
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE X n₁
⊢ 𝟙 X = 0
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithCofibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : Fibration f
⊢ Cofibration f.unop

Tactic:
cofibration_unop_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithCofibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : Fibration f
⊢ Fibration f
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithFibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Fibration f.unop

Tactic:
fibration_unop_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithFibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Cofibration f
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
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
⊢ F.map f₀ = F.map f₁

Tactic:
obtain ⟨P, h, hπ⟩ := hr f₀ f₁ hf
    simp only [← h.h₀, ← h.h₁, Functor.map_comp]
    congr 1
    have := hF _ hπ
    simp [← cancel_mono (F.map P.π), ← Functor.map_comp]

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
x✝ : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ (shiftFunctor C 1).obj W
hT : Triangle.mk a s b ∈ Pretriangulated.distinguishedTriangles
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ (shiftFunctor C 1).obj W'
hT' : Triangle.mk d e f ∈ Pretriangulated.distinguishedTriangles
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right✝ : (Triangle.mk a s b).mor₃ ≫ (shiftFunctor C 1).map c = g ≫ (Triangle.mk d e f).mor₃
⊢ ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
refine ⟨U, e, g, hU, ?_, by cat_disch⟩

Goal state after:
case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
x✝ : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ (shiftFunctor C 1).obj W
hT : Triangle.mk a s b ∈ Pretriangulated.distinguishedTriangles
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ (shiftFunctor C 1).obj W'
hT' : Triangle.mk d e f ∈ Pretriangulated.distinguishedTriangles
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right✝ : (Triangle.mk a s b).mor₃ ≫ (shiftFunctor C 1).map c = g ≫ (Triangle.mk d e f).mor₃
⊢ (A ⊓ B).trW e
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝³³ : Category.{v_1, u_1} C₁
inst✝³² : Category.{v_2, u_2} C₂
inst✝³¹ : Category.{v_3, u_5} C₃
inst✝³⁰ : Category.{v_4, u_6} C₄
inst✝²⁹ : Category.{v_5, u_3} C₁₂
inst✝²⁸ : Category.{v_6, u_4} C₂₃
inst✝²⁷ : HasZeroMorphisms C₁
inst✝²⁶ : HasZeroMorphisms C₂
inst✝²⁵ : HasZeroMorphisms C₃
inst✝²⁴ : Preadditive C₁₂
inst✝²³ : Preadditive C₂₃
inst✝²² : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝²¹ : F₁₂.PreservesZeroMorphisms
inst✝²⁰ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁹ : G.Additive
inst✝¹⁸ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹⁷ : G₂₃.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁵ : F.PreservesZeroMorphisms
inst✝¹⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝¹³ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝¹² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹¹ : TotalComplexShape c₁₂ c₃ c₄
inst✝¹⁰ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁹ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁸ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝⁷ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝⁶ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝⁵ : DecidableEq ι₁₂
inst✝⁴ : DecidableEq ι₂₃
inst✝³ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝² : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝¹ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
⊢ ∀ (i j : ι₄),
    c₄.Rel i j →
      (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ i).hom ≫
          (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).d i j =
        ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).d i j ≫
          (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom

Tactic:
intro j j' _
    simp only [mapBifunctor₁₂.d_eq, mapBifunctor₂₃.d_eq _ _ _ _ _ c₁₂,
      Preadditive.add_comp, Preadditive.comp_add,
      mapBifunctorAssociatorX_hom_D₁, mapBifunctorAssociatorX_hom_D₂,
      mapBifunctorAssociatorX_hom_D₃]

Goal state after:
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
a : ℤ
⊢ triangleFunctorNatTransOfLE t a a ⋯ = 𝟙 (triangleFunctor t a)

Tactic:
by
  apply NatTrans.ext
  ext1 X
  exact triangle_map_ext t (triangleFunctor_obj_distinguished _ _ _)
    (triangleFunctor_obj_distinguished _ _ _) (a - 1) a inferInstance inferInstance (by simp)

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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
⊢ (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful

Tactic:
let : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor
    (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
    ⟨Functor.isoWhiskerLeft A.opEquivalence.functor
      (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm)⟩

Goal state after:
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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
⊢ (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful
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
n m : ℤ
hnm : n + 1 = m
⊢ (↑(cocycle₁' sq hsq)).v n m hnm ≫ p.f m = 0

Tactic:
have fac_right (k : ℤ) := (hsq k).fac_right

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
n m : ℤ
hnm : n + 1 = m
fac_right :
  ∀ (k : ℤ),
    (hsq k).l ≫ (HomologicalComplex.eval C (ComplexShape.up ℤ) k).map p =
      (HomologicalComplex.eval C (ComplexShape.up ℤ) k).map b
⊢ (↑(cocycle₁' sq hsq)).v n m hnm ≫ p.f m = 0
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 : ℤ
this :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ ι.f (n + 1) ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0

Tactic:
π_f_cochain₁_v_ι_f_assoc

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 :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case neg.refine_1
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
a b : ℤ
X : C
h : b < a
⊢ (t.truncGELTToLTGE a b).app X ≫ 0 = 𝟙 ((t.truncGELT a b).obj X)

pp: case neg.refine_2
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
a b : ℤ
X : C
h : b < a
⊢ 0 ≫ (t.truncGELTToLTGE a b).app X = 𝟙 ((t.truncLTGE a b).obj X)

Tactic:
all_goals exact IsZero.eq_of_src (t.isZero _ (b-1) a (by lia)) _ _

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

Goal state before:
pp: case refl
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 g x✝ : X ⟶ Y
⊢ W x✝ ↔ W x✝

Tactic:
| refl =>

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
⊢ LeftHomotopyRel f₀ f₁

Tactic:
exact ⟨P,
      ⟨{h := sq.lift
        h₀ := by
          have := coprod.inl ≫= sq.fac_left
          rwa [P.inl_i_assoc, coprod.inl_desc] at this
        h₁ := by
          have := coprod.inr ≫= sq.fac_left
          rwa [P.inr_i_assoc, coprod.inr_desc] at this }⟩⟩

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Injective fun f ↦ f.postcomp g

pp: case right
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Surjective fun f ↦ f.postcomp g

Tactic:
· intro f₀ f₁ h
    obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
    obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
    simp only [postcomp_mk, mk_eq_mk_iff] at h
    obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_cylinder
    have sq : CommSq (coprod.desc f₀ f₁) P.i g h.h := { }
    rw [mk_eq_mk_iff]
    exact ⟨P,
      ⟨{h := sq.lift
        h₀ := by
          have := coprod.inl ≫= sq.fac_left
          rwa [P.inl_i_assoc, coprod.inl_desc] at this
        h₁ := by
          have := coprod.inr ≫= sq.fac_left
          rwa [P.inr_i_assoc, coprod.inr_desc] at this }⟩⟩

Goal state after:
case right
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Surjective fun f ↦ f.postcomp g
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α

Tactic:
intro hα

Goal state after:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
⊢ IsIso α
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α

Tactic:
intro hα

Goal state after:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
⊢ IsIso α