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✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h : RightHomotopyRel f g
⊢ ∃ P, P.IsVeryGood ∧ Nonempty (P.RightHomotopy f g)

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject
  let fac := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
  let P' : PathObject Y :=
    { P := fac.Z
      p₀ := fac.p ≫ P.p₀
      p₁ := fac.p ≫ P.p₁
      ι := fac.i
      weakEquivalence_ι := weakEquivalence_of_postcomp_of_fac fac.fac }
  have : Fibration P'.p := by
    rw [show P'.p = fac.p ≫ P.p by cat_disch]
    infer_instance
  have sq : CommSq (initial.to _) (initial.to _) fac.p h.h := { }
  exact ⟨P', { }, ⟨{ h := sq.lift }⟩⟩

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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp ((δ 0 1 α).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ (l.homOf ≫ p).f n = b.f n

Tactic:
have : ι.f n ≫ p.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hι]

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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp ((δ 0 1 α).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
this : ι.f n ≫ p.f n = 0
⊢ (l.homOf ≫ p).f n = b.f n
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
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
this : coprod.inl ≫ P.i ≫ sq.lift = coprod.inl ≫ coprod.desc f₀ f₁
⊢ P.i₀ ≫ sq.lift = f₀

Tactic:
rwa [P.inl_i_assoc, coprod.inl_desc] at this

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

Goal state before:
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 φ
    obtain ⟨φ, rfl⟩ := φ.mk_surjective
    have sq : CommSq (initial.to Y) (initial.to X) g φ := { }
    exact ⟨mk sq.lift, by simp⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
⊢ Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) { hom := f })

Tactic:
obtain ⟨d, _, _⟩ : ∃ (d : ℤ), K.IsStrictlyGE (d + 1) ∧ L.IsStrictlyGE d :=
      ⟨min (n - 1) m, K.isStrictlyGE_of_ge _ n (by grind),
        L.isStrictlyGE_of_ge _ m (by simp)⟩

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝ : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
⊢ Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) { hom := f })
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
⊢ Nonempty ((cofibrations (Plus C)).MapFactorizationData (trivialFibrations (Plus C)) { hom := f })

Tactic:
obtain ⟨d, _, _⟩ : ∃ (d : ℤ), K.IsStrictlyGE (d + 1) ∧ L.IsStrictlyGE d :=
      ⟨min (n - 1) m, K.isStrictlyGE_of_ge _ n (by grind),
        L.isStrictlyGE_of_ge _ m (by simp)⟩

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝ : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
⊢ Nonempty ((cofibrations (Plus C)).MapFactorizationData (trivialFibrations (Plus C)) { hom := f })
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 (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ Φ.IsRightDerivabilityStructure

Tactic:
rw [Φ.isRightDerivabilityStructure_iff (Φ.functor ⋙ W₂.Q) W₂.Q (𝟭 _)
    (Functor.rightUnitor _).symm, TwoSquare.guitartExact_iff_isConnected_downwards]

Goal state after:
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 (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ ∀ {X₂ : C₂} {X₃ : W₂.Localization} (g : W₂.Q.obj X₂ ⟶ (𝟭 W₂.Localization).obj X₃),
    IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom g)
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasRightDerivedFunctor W
⊢ L.HasLeftKanExtension F

Tactic:
by
  simpa only [← hasRightDerivedFunctor_iff F L W]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
this✝ : K.obj.IsGE n
L : CochainComplex C ℤ
w✝¹ : L.IsStrictlyGE n
e : K.obj ≅ DerivedCategory.Q.obj L
M : CochainComplex.Plus (InjectiveObject C)
w✝ : M.obj.IsStrictlyGE n
i : { obj := L, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj M
hi : CochainComplex.Plus.quasiIso C i
this : QuasiIso i.hom
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), Nonempty (Q.obj ((InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)

Tactic:
exact ⟨M, inferInstance,
    ⟨DerivedCategory.Plus.ι.preimageIso ((asIso (DerivedCategory.Q.map i.hom)).symm ≪≫ e.symm)⟩⟩

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Category.{v_2, u_2} H
inst✝¹ : EnoughInjectives C
inst✝ : HasDerivedCategory C
K : DerivedCategory.Plus C
⊢ ((InjectiveObject.ι C).mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh).essImage K

Tactic:
let r : (HomotopyCategory.Plus.localizerMorphism C).RightResolution
        (DerivedCategory.Plus.Qh.objPreimage K) := Classical.arbitrary _

Goal state after:
C : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Category.{v_2, u_2} H
inst✝¹ : EnoughInjectives C
inst✝ : HasDerivedCategory C
K : DerivedCategory.Plus C
r : (localizerMorphism C).RightResolution (DerivedCategory.Plus.Qh.objPreimage K) :=
  Classical.arbitrary ((localizerMorphism C).RightResolution (DerivedCategory.Plus.Qh.objPreimage K))
⊢ ((InjectiveObject.ι C).mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh).essImage K
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ (F.map X.d ≫ η.app X.obj) ≫ (shiftFunctor D 1).map (F.map X.d ≫ η.app X.obj) = 0

Tactic:
by
        rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : S))]
        slice_lhs 2 3 => rw [← η.naturality X.d]
        rw [Functor.comp_map]
        slice_lhs 1 2 => rw [← F.map_comp, X.d_squared, hF]
        rw [zero_comp, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map X.d ≫
      (shiftComm X.obj 1 n).hom ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map X.d) ≫
          (CategoryTheory.shiftFunctor C 1).map (shiftComm X.obj 1 n).hom =
    0

Tactic:
shiftComm_hom_comp_assoc,

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map X.d ≫
      (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map X.d) ≫
        (shiftComm ((CategoryTheory.shiftFunctor C 1).obj X.obj) 1 n).hom ≫
          (CategoryTheory.shiftFunctor C 1).map (shiftComm X.obj 1 n).hom =
    0
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ (J ^ 0).radical

pp: case succ
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
n : ℕ
⊢ J ≤ (J ^ (n + 1)).radical

Tactic:
· simp [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top]

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
n : ℕ
⊢ J ≤ (J ^ (n + 1)).radical
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ IsZero ((F.leftDerived (n + 1)).obj X)

Tactic:
refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoLeftDerivedObj F (n + 1))
  erw [← HomologicalComplex.exactAt_iff_isZero_homology]
  exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫ mapBifunctor.d₂ (tensorUnit C c) K (curriedTensor C) c 0 i j =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j j ⋯

Tactic:
rw [mapBifunctor.d₂_eq _ _ _ _ _ hij _ (by simp)]

Goal state after:
case pos
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫
        (c.ε₂ c c (0, i) •
          ((curriedTensor C).obj ((tensorUnit C c).X 0)).map (K.d i j) ≫
            (tensorUnit C c).ιMapBifunctor K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j j ⋯
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ L₂ : HomologicalComplex C c
g : K₂ ⟶ L₂
⊢ (forget C c).map (K₁ ◁ g) =
    (Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj K₂)).inv ≫
      (forget C c).obj K₁ ◁ (forget C c).map g ≫ (Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj L₂)).hom

Tactic:
by
    dsimp [forget]
    rw [comp_id]
    erw [id_comp]
    rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ L₁ : HomologicalComplex C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex C c
⊢ (forget C c).map (f ▷ K₂) =
    (Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj K₂)).inv ≫
      (forget C c).map f ▷ (forget C c).obj K₂ ≫ (Iso.refl ((forget C c).obj L₁ ⊗ (forget C c).obj K₂)).hom

Tactic:
by
    dsimp [forget]
    rw [comp_id]
    erw [id_comp]
    rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ L₁ K₂ L₂ : HomologicalComplex C c
f : K₁ ⟶ L₁
g : K₂ ⟶ L₂
⊢ (forget C c).map (f ⊗ₘ g) =
    (Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj K₂)).inv ≫
      ((forget C c).map f ⊗ₘ (forget C c).map g) ≫ (Iso.refl ((forget C c).obj L₁ ⊗ (forget C c).obj L₂)).hom

Tactic:
by
    dsimp [forget]
    rw [comp_id]
    erw [id_comp]
    rfl

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst✝ : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
⊢ r (i₁, 0, i₃) = π (i₁, i₃)

Tactic:
by
  rw [← τ.hp₂₃, τ.h₃ i₃]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α

Tactic:
by
  have h := (X.δ' n₀ n₁ hn₁).naturality
    (homMk₂ (α.app 0) (α.app 1) (β.app 1) (naturality' α 0 1)
      (by simpa only [hαβ] using! naturality' β 0 1) : mk₂ f g ⟶ mk₂ f' g')
  dsimp at h
  convert! h <;> cat_disch

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 ≫
    X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ▷ X₄ i₄ ≫
      ιTensorObj₃ X₁ (tensorObj X₂ X₃) X₄ i₁ (i₂ + i₃) i₄ j ⋯ ≫
        (associator X₁ (tensorObj X₂ X₃) X₄).inv j ≫ tensorHom (associator X₁ X₂ X₃).inv (𝟙 X₄) j

Tactic:
ιTensorObj₃_associator_inv_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₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ▷ X₄ i₄ ≫
      (α_ (X₁ i₁) (tensorObj X₂ X₃ (i₂ + i₃)) (X₄ i₄)).inv ≫
        ιTensorObj₃' X₁ (tensorObj X₂ X₃) X₄ i₁ (i₂ + i₃) i₄ j ⋯ ≫ tensorHom (associator X₁ X₂ X₃).inv (𝟙 X₄) j
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₂ ◁ ιTensorObj X₃ X₄ i₃ i₄ (i₃ + i₄) ⋯ ≫
    ιTensorObj₃ X₁ X₂ (tensorObj X₃ X₄) i₁ i₂ (i₃ + i₄) j ⋯ ≫
      (associator X₁ X₂ (tensorObj X₃ X₄)).inv j ≫ (associator (tensorObj X₁ X₂) X₃ X₄).inv j

Tactic:
ιTensorObj₃_associator_inv_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₂ ◁ ιTensorObj X₃ X₄ i₃ i₄ (i₃ + i₄) ⋯ ≫
    (α_ (X₁ i₁) (X₂ i₂) (tensorObj X₃ X₄ (i₃ + i₄))).inv ≫
      ιTensorObj₃' X₁ X₂ (tensorObj X₃ X₄) i₁ i₂ (i₃ + i₄) j ⋯ ≫ (associator (tensorObj X₁ X₂) X₃ X₄).inv j