mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ toHoCat.map f = toHoCat.map g ↔ homRel C f g

Tactic:
by
  dsimp [toHoCat]
  rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isCofibrant_src.eqvGen_eq]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution X₂)
inst✝² : Φ.arrow.HasLeftResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ Φ.IsLeftDerivabilityStructure

Tactic:
by
  rw [isLeftDerivabilityStructure_iff_op]
  have : Φ.op.arrow.HasRightResolutions := fun f ↦ by
    let R : Φ.arrow.LeftResolution (Arrow.mk f.hom.unop) := Classical.arbitrary _
    exact ⟨{
      X₁ := Arrow.mk R.X₁.hom.op
      w := Arrow.homMk R.w.right.op R.w.left.op (Quiver.Hom.unop_inj R.w.w.symm)
      hw := ⟨R.hw.right, R.hw.left⟩ }⟩
  have (X₂ : C₂ᵒᵖ) : IsConnected (Φ.op.RightResolution X₂) :=
    isConnected_of_equivalent (LeftResolution.opEquivalence Φ X₂.unop)
  exact IsRightDerivabilityStructure.mk' _

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} C₃
inst✝² : Category.{v₄, u₄} C₄
inst✝¹ : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
F : C₂ ⥤ D
E : R.LeftExtension F
w : TwoSquare T L R B
X₃ : C₃
inst✝ : (w.costructuredArrowRightwards X₃).Final
⊢ (E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃ ≃
    IsColimit (Cocone.whisker (w.costructuredArrowRightwards X₃) (E.coconeAt (B.obj X₃)))

Tactic:
exact IsColimit.equivIsoColimit (Cocone.ext (Iso.refl _))

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseRightDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
⊢ L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
have := Localization.essSurj L W

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseRightDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ L.HasPointwiseLeftKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
hF : F.HasPointwiseRightDerivedFunctor W₂
X₁ : C₁
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor.obj X₁)

Tactic:
apply hF

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
⊢ K.IsKProjective ↔
    (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)

Tactic:
by
  refine ⟨fun _ L f hL ↦ ?_,
      fun hK ↦ ⟨fun {L} f hL ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩
  · obtain ⟨L, rfl⟩ := HomotopyCategory.quotient_obj_surjective L
    obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f
    rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL
    rw [HomotopyCategory.eq_of_homotopy f 0 (IsKProjective.homotopyZero f hL), Functor.map_zero]
  · rw [← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL
    rw [hK ((HomotopyCategory.quotient _ _).map f) hL, Functor.map_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
      F.mapDerivedCategory.map ((Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
      F.mapDerivedCategoryFactors.hom.app
          ((shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle S.f).obj₁) ≫
        Q.map ((Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app S.X₁) ≫
          (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
simp [NatTrans.shift_app, Functor.commShiftIso_comp_hom_app, Functor.commShiftIso_comp_inv_app,
    ← Functor.map_comp_assoc]

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

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ (fun b_1 ↦ b_1 + { as := 1 }.as • b) x = (fun b_1 ↦ b_1 + { as := 1 }.as • b) y

Tactic:
cases h

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ (fun b_1 ↦ b_1 + { as := 1 }.as • b) x = (fun b_1 ↦ b_1 + { as := 1 }.as • b) x
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom ⋯

Tactic:
cases h

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x y : β
h : x = y
⊢ X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h

Tactic:
cases h

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y z : β
h : y = z
⊢ X.d x y ≫ eqToHom ⋯ = X.d x z

Tactic:
cases h

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ X.d x y ≫ eqToHom ⋯ = X.d x y
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i j
⊢ ¬(j = i ∧ k = j ∧ ¬i = j)

Tactic:
tauto

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
hj : ¬j = i₁
⊢ ¬(i = i ∧ j = i₁ ∧ ¬i = i₁)

Tactic:
tauto

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : ¬i = i₀
⊢ ¬(i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁)

Tactic:
tauto

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
a b : ι
ha : a ≠ i₀
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
tauto

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
a b : ι
hb : b ≠ i₁
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
f : HomSubtype S C X✝ Y✝
⊢ X✝.d ≫ (shiftFunctor C 1).map (ConcreteCategory.ofHom ↑f) = ConcreteCategory.ofHom ↑f ≫ Y✝.d

Tactic:
by simpa [ConcreteCategory.hom_ofHom] using f.2

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
⊢ h.d n m ≫ h.d m p = 0

Tactic:
by_cases hnm : n + 1 = m

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
⊢ h.d n m ≫ h.d m p = 0

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : ¬n + 1 = m
⊢ h.d n m ≫ h.d m p = 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n : ℕ
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
hmp : Int.ofNat (n + 1) + 1 = Int.ofNat (n + 2)
⊢ h.d (Int.ofNat n) (Int.ofNat (n + 1)) ≫ h.d (Int.ofNat (n + 1)) (Int.ofNat (n + 2)) = 0

Tactic:
simp only [Int.ofNat_eq_natCast, X_ofNat, d_ofNat, HomologicalComplex.d_comp_d]

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

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∃ k, c.Rel j k ∧ j ≠ k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

Tactic:
tauto

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

Goal state before:
pp: case neg.inr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∀ (k : ι), ¬c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

Tactic:
tauto

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : Abelian V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (T ⥤ V) c
f : K₁ ⟶ K₂
⊢ (∀ (i : ι) (t : T), QuasiIsoAt ((((evaluation T V).obj t).mapHomologicalComplex c).map f) i) ↔
    ∀ (t : T) (i : ι), QuasiIsoAt ((((evaluation T V).obj t).mapHomologicalComplex c).map f) i

Tactic:
tauto

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 q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ δ n (n + 1) (Cochain.toSingleMk f h) = 0

Tactic:
Cochain.δ_toSingleMk _ _ _ p' (by lia),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ (n + 1).negOnePow •
      Cochain.toSingleMk (K.d p' p ≫ f) (CochainComplex.HomComplex.Cocycle.toSingleMk._proof_1 p q n h p' hp') =
    0
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 ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : (n + 1).negOnePow • δ n (n + 1) (Cochain.toSingleMk f h) = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
Cochain.δ_toSingleMk _ _ _ p' (by lia),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : (n + 1).negOnePow • (n + 1).negOnePow • Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' 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 ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : 1 • Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
one_smul

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: case neg
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
hi : ¬i = 0
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(i, j'), h⟩ ≫
      e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
    s.inj ⟨(i, j'), h⟩

Tactic:
apply IsInitial.hom_ext
        exact mapBifunctorObjSingle₀ObjIsInitial _ _ _ _ hi

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝²⁵ : AddMonoid I
C : Type u_1
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝²² : X₁.HasTensor X₂
inst✝²¹ : X₂.HasTensor X₃
inst✝²⁰ : X₃.HasTensor X₄
inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄
inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄
inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄
inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)
inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)
inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄
inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄
inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄
inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄
inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄
inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)
inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄
j i₁ i₂ i₃ i₄ : I
h : i₁ + i₂ + i₃ + i₄ = j
| (α_ (X₁ i₁) (X₂ i₂) (X₃ i₃ ⊗ X₄ i₄)).inv ≫
    ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ (X₃ i₃ ⊗ X₄ i₄) ≫
      (α_ (tensorObj X₁ X₂ (i₁ + i₂)) (X₃ i₃) (X₄ i₄)).inv ≫ ιTensorObj₃' (tensorObj X₁ X₂) X₃ X₄ (i₁ + i₂) i₃ i₄ j h

Tactic:
whiskerRight_tensor_assoc,

Goal state after:
I : Type u
inst✝²⁵ : AddMonoid I
C : Type u_1
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝²² : X₁.HasTensor X₂
inst✝²¹ : X₂.HasTensor X₃
inst✝²⁰ : X₃.HasTensor X₄
inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄
inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄
inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄
inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)
inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)
inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄
inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄
inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄
inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄
inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄
inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)
inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄
j i₁ i₂ i₃ i₄ : I
h : i₁ + i₂ + i₃ + i₄ = j
| (α_ (X₁ i₁) (X₂ i₂) (X₃ i₃ ⊗ X₄ i₄)).inv ≫
    (α_ (X₁ i₁ ⊗ X₂ i₂) (X₃ i₃) (X₄ i₄)).inv ≫
      ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ X₃ i₃ ▷ X₄ i₄ ≫
        (α_ (tensorObj X₁ X₂ (i₁ + i₂)) (X₃ i₃) (X₄ i₄)).hom ≫
          (α_ (tensorObj X₁ X₂ (i₁ + i₂)) (X₃ i₃) (X₄ i₄)).inv ≫
            ιTensorObj₃' (tensorObj X₁ X₂) X₃ X₄ (i₁ + i₂) i₃ i₄ j h
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₃' : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₃' : i₂ ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X.cyclesMap f₁ f₂ f₁ f₂ (𝟙 (mk₂ f₁ f₂)) n₁)

Tactic:
rw [X.cyclesMap_id]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₃' : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₃' : i₂ ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (𝟙 (X.cycles f₁ f₂ n₁))
Module: Mathlib.Algebra.Homology.SpectralObject.Homology

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯

Tactic:
have hy₂' := hy₂ =≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ≫ X.ιE ..

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' :
  (π₁ ≫ x₂) ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ =
    (y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯) ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : n + 1 = n'
⊢ ((X.spectralSequence data).page r₀ ⋯).d pq pq' =
    (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn).hom ≫
      X.δ (homOfLE ⋯) (homOfLE ⋯) n n' hn' ≫ (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯).inv

Tactic:
by
  simpa [X.spectralSequenceFirstPageXIso_hom data pq j k hj hk (n - 1) n n',
    ← X.d_EIsoH_hom_assoc _ _ (n - 1) n n' (n' + 1),
    X.spectralSequenceFirstPageXIso_inv data pq' i j hi _ _ n' _ _ hn' _]
    using spectralSequence_page_d_eq _ _ _ _ _ _ hpq ..

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → (partialSups (⇑OrderDual.toDual ∘ f)) n = (partialSups (⇑OrderDual.toDual ∘ f)) m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → OrderDual.toDual f (m + 1) = ⊤

Tactic:
refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → (partialSups (⇑OrderDual.toDual ∘ f)) n = (partialSups (⇑OrderDual.toDual ∘ f)) m
m : ℕ
p : n ≤ m
⊢ (partialSups (⇑OrderDual.toDual ∘ f)) m ⊔ OrderDual.toDual (f (m + 1)) = (partialSups (⇑OrderDual.toDual ∘ f)) m