mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
a b : ℤ
⊢ NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F (a + b)) ⋯ =
    CommShift.isoAdd (NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F a) ⋯)
      (NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F b) ⋯)

Tactic:
by
    ext K₂ n
    dsimp
    ext p q h
    dsimp at h
    simp [CochainComplex.ι_mapBifunctorShift₂Iso_hom_f _ _ F (a + b) p q n h
        (q + a + b) (n + a + b) (by lia) (by lia),
      CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc _ _ F b p q n h _ _ rfl rfl,
      CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc _ _ F a p (q + b) (n + b)
        (by lia) (q + a + b) (n + a + b) (by lia) (by lia), smul_smul,
        ← Int.negOnePow_add, CochainComplex.shiftFunctorAdd_eq,
        add_comm (p * b), mul_add, XIsoOfEq]

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 sq.kernelFork
s : PullbackCone f g
⊢ h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ≫ fst = s.fst

Tactic:
simpa using

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 sq.kernelFork
s : PullbackCone f g
⊢ h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ≫ fst = s.fst
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 sq.kernelFork
s : PullbackCone f g
⊢ h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ≫ snd = s.snd

Tactic:
simpa using

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 sq.kernelFork
s : PullbackCone f g
⊢ h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯) ≫ snd = s.snd
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 ≫ Fork.ι ⋯.kernelFork = 0 ≫ Fork.ι ⋯.kernelFork

Tactic:
simpa using

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₄
h : IsPullback fst snd f g
P✝ : C
b : P✝ ⟶ ⋯.shortComplex'.X₁
hb : b ≫ ⋯.shortComplex'.f = 0
⊢ b ≫ biprod.lift fst snd = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ (↑(sequence φ x₀ n₁)).EqUpTo (↑(sequence φ x₀ n₂)) (p₀ + ↑n₁)

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  clear h
  induction k generalizing n₁ with
  | zero => intro _ _ _ _; simp
  | succ k hk =>
    intro p q hpq hp
    rw [hk n₁ p q hpq hp, ← hφ (n₁ + k) (sequence φ x₀ (n₁ + k)) p q hpq (by lia)]
    dsimp [sequence]

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 ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (hS.δ i j hij)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.homologyπ i))) (S.X₃.cyclesMk x₃ j ⋯ hx₃)) =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.homologyπ j))) (S.X₁.cyclesMk x₁ k hk ⋯)

Tactic:
refine hS.δ_apply' i j hij _ ((forget₂ C Ab).map (S.X₂.pOpcycles i) x₂) _ ?_ ?_
  · rw [← ConcreteCategory.forget₂_comp_apply, ← ConcreteCategory.forget₂_comp_apply,
      HomologicalComplex.p_opcyclesMap, Functor.map_comp, ConcreteCategory.comp_apply,
      HomologicalComplex.homology_π_ι, ConcreteCategory.forget₂_comp_apply, hx₂,
      HomologicalComplex.i_cyclesMk]
  · apply (Preadditive.mono_iff_injective (S.X₂.iCycles j)).1 inferInstance
    conv_lhs =>
      rw [← ConcreteCategory.forget₂_comp_apply, HomologicalComplex.cyclesMap_i,
        ConcreteCategory.forget₂_comp_apply, HomologicalComplex.i_cyclesMk, hx₁]
    conv_rhs =>
      rw [← ConcreteCategory.forget₂_comp_apply, ← ConcreteCategory.forget₂_comp_apply,
        HomologicalComplex.pOpcycles_opcyclesToCycles_assoc, HomologicalComplex.toCycles_i]

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

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

Tactic:
mk_eq_zero_iff,

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x y : Cocycle K L n
h : toHom (mk x) = toHom (mk y)
⊢ x - y ∈ coboundaries K L n
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
this : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
α₁ α₂ : X₂ ⟶ Y
hα : (fun g ↦ f ≫ g) α₁ = (fun g ↦ f ≫ g) α₂
⊢ α₁ = α₂

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
this : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
α₁ α₂ : X₂ ⟶ Y
hα : (fun g ↦ f ≫ g) α₁ = (fun g ↦ f ≫ g) α₂
⊢ α₁ = α₂
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
this : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
α₁ α₂ : X₂ ⟶ Y
hα : (fun g ↦ f ≫ g) α₁ = (fun g ↦ f ≫ g) α₂
⊢ f ≫ (α₁ - α₂) = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
this : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
α₁ α₂ : X₂ ⟶ Y
hα : (fun g ↦ f ≫ g) α₁ = (fun g ↦ f ≫ g) α₂
⊢ f ≫ α₁ = f ≫ α₂
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ (shiftFunctor C 1).obj Y₁
hT : Triangle.mk f h g ∈ distinguishedTriangles
hY₁ : P Y₁
this : ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0
α₁ α₂ : X ⟶ Y₂
hα : (fun f ↦ f ≫ h) α₁ = (fun f ↦ f ≫ h) α₂
⊢ α₁ = α₂

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ (shiftFunctor C 1).obj Y₁
hT : Triangle.mk f h g ∈ distinguishedTriangles
hY₁ : P Y₁
this : ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0
α₁ α₂ : X ⟶ Y₂
hα : (fun f ↦ f ≫ h) α₁ = (fun f ↦ f ≫ h) α₂
⊢ α₁ = α₂
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (extendMap f e).f (e.f i) =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) + (extendMap g e).f (e.f i)

Tactic:
extendMap_f _ _ rfl,

Goal state after:
case pos
ι : 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
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) + (extendMap g e).f (e.f i)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) + (extendMap g e).f (e.f i)

Tactic:
extendMap_f _ _ rfl,

Goal state after:
case pos
ι : 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
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
Y : C
hY : P.trW.isLocal Y
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = g

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.trW g

Goal state after:
case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
Y : C
hY : P.trW.isLocal Y
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.RightFraction X Y
hφ : g = φ.map L ⋯
⊢ ∃ a, L.map a = g
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
Y : C
hY : P.trW.isLocal Y
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = g

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.trW g
    obtain ⟨α, hα⟩ := (hY _ φ.hs).2 φ.f
    refine ⟨α, ?_⟩
    rw [hφ, ← cancel_epi (L.map φ.s), MorphismProperty.RightFraction.map_s_comp_map,
      ← hα, Functor.map_comp]

Goal state after:
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 j : ι
hij : ¬c.Rel j i
⊢ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom = 0

Tactic:
by rw [h.zero _ _ (by rwa [e.rel_iff]), zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
⊢ Nonempty (Homotopy f 0)

Tactic:
let X (n : ℕ) : Set (Cochain K L (-1)) :=
      Set.ofPred (fun α => (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (n + d - 1))

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
⊢ Nonempty (Homotopy f 0)
Module: Mathlib.Algebra.Homology.HomotopyFiber

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
α : Type u_2
c : ComplexShape α
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : α), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasPathObject
i : α
h₁ : IsZero (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)
⊢ IsZero ((eval Cᵒᵖ c.symm i).obj K.op ⊞ (eval Cᵒᵖ c.symm i).obj K.op)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
α : Type u_2
c : ComplexShape α
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : α), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasPathObject
i : α
h₁ : IsZero (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)
⊢ IsZero (op (K.X i))
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ i < n, IsZero ((homologyFunctor C i).obj X)
i : ℤ
hi : i < n
⊢ IsZero (HomologicalComplex.homology (Q.objPreimage X) i)

Tactic:
apply (hX i hi).of_iso

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ i < n, IsZero ((homologyFunctor C i).obj X)
i : ℤ
hi : i < n
⊢ HomologicalComplex.homology (Q.objPreimage X) i ≅ (homologyFunctor C i).obj X
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)
i : ℤ
hi : n < i
⊢ IsZero (HomologicalComplex.homology (Q.objPreimage X) i)

Tactic:
apply (hX i hi).of_iso

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)
i : ℤ
hi : n < i
⊢ HomologicalComplex.homology (Q.objPreimage X) i ≅ (homologyFunctor C i).obj X
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

Tactic:
rw [← le_llp_iff_le_rlp]

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts ≤ T.rlp.llp
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ n.negOnePow • (δ m n (f.rightUnshift m ⋯)).rightShift n 0 ⋯ = δ (-1) 0 f

Tactic:
Cochain.δ_rightUnshift _ _ _ _ 0 (by simp)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ n.negOnePow • (n.negOnePow • (δ (-1) 0 f).rightUnshift n ⋯).rightShift n 0 ⋯ = δ (-1) 0 f
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

Tactic:
rw [← le_llp_iff_le_rlp]

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

Tactic:
rw [← le_llp_iff_le_rlp]

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.retracts ≤ T.rlp.llp
Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
h : W₁.MapFactorizationData W₂ i
this : HasLiftingProperty i h.p
⊢ W₁ i

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
h : W₁.MapFactorizationData W₂ i
this : HasLiftingProperty i h.p
⊢ W₁ i
Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
h : W₁.MapFactorizationData W₂ p
this : HasLiftingProperty h.i p
⊢ W₂ p

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
h : W₁.MapFactorizationData W₂ p
this : HasLiftingProperty h.i p
⊢ W₂ p
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:
by
  rwa [fibration_unop_iff]

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
J✝ : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst✝³ : HasCoproduct X
inst✝² : HasCoproduct Y
h : ∀ (i : J), Cofibration (f i)
inst✝¹ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝ : ∀ (i : J), WeakEquivalence (f i)
⊢ WeakEquivalence (Limits.Sigma.map f)

Tactic:
by
  rw [weakEquivalence_iff]
  exact (MorphismProperty.colimMap (W := (trivialCofibrations C)) _
    (fun ⟨i⟩ ↦ mem_trivialCofibrations (f i))).2

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 : C
f : X ⟶ Y
inst✝¹ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝ : IsIso f
this : trivialCofibrations C f
⊢ Cofibration f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y : C
f : X ⟶ Y
inst✝¹ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝ : IsIso f
this : trivialCofibrations C f
⊢ cofibrations C f
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 : C
f : X ⟶ Y
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : IsIso f
this : trivialFibrations C f
⊢ Fibration f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y : C
f : X ⟶ Y
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : IsIso f
this : trivialFibrations C f
⊢ fibrations C f
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 : C
f : X ⟶ Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) f
⊢ Cofibration h.i

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CategoryWithWeakEquivalences C
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithFibrations C
X Y : C
f : X ⟶ Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) f
⊢ cofibrations C h.i