mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map f ≫
        (NatIso.ofComponents
            (fun X ↦
              {
                hom :=
                  {
                    f :=
                      𝟙
                        (((functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj
                                Y).obj
                            X).X,
                    comm := ⋯ },
                inv := { f := 𝟙 ((((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).obj Y).obj X).X, comm := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ })
            ⋯).hom =
      (NatIso.ofComponents
            (fun X_1 ↦
              {
                hom :=
                  {
                    f :=
                      𝟙
                        (((functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj
                                X).obj
                            X_1).X,
                    comm := ⋯ },
                inv := { f := 𝟙 ((((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).obj X).obj X_1).X, comm := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ })
            ⋯).hom ≫
        ((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X Y : Karoubi C
f : X ⟶ Y
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
by
        dsimp at τ ⊢
        have h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f := by simp
        have h₂ := τ.naturality f.f
        have h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p := by simp
        dsimp at h₂
        rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]

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

Goal state before:
pp: case pos
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:
subst hi

Goal state after:
case pos
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)
j' : J
h : (0, j') ∈ p ⁻¹' {j}
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j'), h⟩ ≫
      e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
    s.inj ⟨(0, j'), h⟩
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
⊢ F.whiskerLeft π₁Toπ₂ ≫ F.whiskerLeft π₂Toπ₃ = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : J ⥤ ShortComplex C
φ : X✝ ⟶ Y✝
⊢ whiskerRight φ π₁ ≫
      { X₁ := Y✝ ⋙ π₁, X₂ := Y✝ ⋙ π₂, X₃ := Y✝ ⋙ π₃, f := Y✝.whiskerLeft π₁Toπ₂, g := Y✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.f =
    { X₁ := X✝ ⋙ π₁, X₂ := X✝ ⋙ π₂, X₃ := X✝ ⋙ π₃, f := X✝.whiskerLeft π₁Toπ₂, g := X✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.f ≫
      whiskerRight φ π₂

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : J ⥤ ShortComplex C
φ : X✝ ⟶ Y✝
⊢ whiskerRight φ π₂ ≫
      { X₁ := Y✝ ⋙ π₁, X₂ := Y✝ ⋙ π₂, X₃ := Y✝ ⋙ π₃, f := Y✝.whiskerLeft π₁Toπ₂, g := Y✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.g =
    { X₁ := X✝ ⋙ π₁, X₂ := X✝ ⋙ π₂, X₃ := X✝ ⋙ π₃, f := X✝.whiskerLeft π₁Toπ₂, g := X✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.g ≫
      whiskerRight φ π₃

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.obj x)) ⋯).hom ≫
      ((functor J C ⋙ inverse J C).obj x✝).f =
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).f ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)) ⋯).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)) ⋯).hom ≫
      ((functor J C ⋙ inverse J C).obj x✝).g =
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).g ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.obj x)) ⋯).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
⊢ ∀ {X Y : ShortComplex (J ⥤ C)} (f : X ⟶ Y),
    (𝟭 (ShortComplex (J ⥤ C))).map f ≫
        (isoMk (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj Y).X₁.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj Y).X₂.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj Y).X₃.obj x)) ⋯) ⋯ ⋯).hom =
      (isoMk (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj X).X₁.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj X).X₂.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj X).X₃.obj x)) ⋯) ⋯ ⋯).hom ≫
        (functor J C ⋙ inverse J C).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : J ⥤ ShortComplex C
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((inverse J C ⋙ functor J C).obj x✝).map f ≫
        (isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj Y).X₁)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj Y).X₂)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj Y).X₃) ⋯ ⋯).hom =
      (isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj X).X₁)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj X).X₂)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj X).X₃) ⋯ ⋯).hom ≫
        ((𝟭 (J ⥤ ShortComplex C)).obj x✝).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
⊢ ∀ {X Y : J ⥤ ShortComplex C} (f : X ⟶ Y),
    (inverse J C ⋙ functor J C).map f ≫
        (NatIso.ofComponents
            (fun x ↦
              isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj Y).obj x).X₁)
                (Iso.refl (((inverse J C ⋙ functor J C).obj Y).obj x).X₂)
                (Iso.refl (((inverse J C ⋙ functor J C).obj Y).obj x).X₃) ⋯ ⋯)
            ⋯).hom =
      (NatIso.ofComponents
            (fun x ↦
              isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj X).obj x).X₁)
                (Iso.refl (((inverse J C ⋙ functor J C).obj X).obj x).X₂)
                (Iso.refl (((inverse J C ⋙ functor J C).obj X).obj x).X₃) ⋯ ⋯)
            ⋯).hom ≫
        (𝟭 (J ⥤ ShortComplex C)).map f

Tactic:
by cat_disch

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

Goal state before:
pp: case pos
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 : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
j' : J
i : I
h : (j', i) ∈ p ⁻¹' {j}
hi : i = 0
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j', i), h⟩ ≫
      e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
    s.inj ⟨(j', i), h⟩

Tactic:
subst hi

Goal state after:
case pos
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 : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
j' : J
h : (j', 0) ∈ p ⁻¹' {j}
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j', 0), h⟩ ≫
      e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
    s.inj ⟨(j', 0), h⟩
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (x y : R) (b : S₁ ⟶ S₂), (x * y) • b = x • y • b

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (b : S₁ ⟶ S₂), 1 • b = b

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (a : R) (x y : S₁ ⟶ S₂), a • (x + y) = a • x + a • y

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (r s : R) (x : S₁ ⟶ S₂), (r + s) • x = r • x + s • x

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (x : S₁ ⟶ S₂), 0 • x = 0

Tactic:
by 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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ hi ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j ⋯

Tactic:
subst hi

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 (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ (i₂ + i₃ + i₄) ⋯ ≫
      ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ (i₂ + i₃ + i₄) j ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, 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'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ homMk₁ (α.app 0) (α.app 1) ⋯ ≫ homMk₁ (α'.app 0) (α'.app 1) ⋯ = homMk₁ ((α ≫ α').app 0) ((α ≫ α').app 1) ⋯

Tactic:
by cat_disch

Goal state after:
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₃
this : Epi (X.cyclesMap f₁ f₂ f₁ f₂ (𝟙 (mk₂ f₁ f₂)) n₁)
⊢ 𝟙 (mk₂ f₁ f₂) = homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯

Tactic:
by cat_disch

Goal state after:
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₄ 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₃
⊢ 𝟙 (mk₂ f₄ f₅) =
    homMk₂ ((fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃).app 1) ((fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃).app 2)
      ((fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃).app 3) ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ 𝟙 (mk₁ f₃) = homMk₁ ((threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 1) ((threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 2) ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A✝ : C
z₀ :
  A✝ ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A✝
w✝ : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
⊢ 𝟙 (mk₁ f₁) = homMk₁ ((threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 0) ((threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 1) ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Order.Fin.Clamp

Goal state before:
pp: m a : ℕ
⊢ ∀ ⦃b : ℕ⦄, a ≤ b → (fun n ↦ clamp n m) a ≤ (fun n ↦ clamp n m) b

Tactic:
b

Goal state after:
m a b : ℕ
⊢ a ≤ b → (fun n ↦ clamp n m) a ≤ (fun n ↦ clamp n m) b
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
⊢ IsZero ((X.H n).obj (mk₁ f))

Tactic:
let e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl _) (asIso f) (by simp)

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl ((mk₁ (𝟙 i)).obj' 0 homMk₁._proof_4)) (asIso f) ⋯
⊢ IsZero ((X.H n).obj (mk₁ f))
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).f ≫ x = 0

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
A : C
x : A ⟶ (X.H n₁).obj (mk₁ f₂₃)
h : x ≫ (X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0
hn₂ : n₁ + 1 = n₂
h' : x ≫ X.δ f₁ f₂₃ n₁ n₂ hn₂ = 0
hn₁ : n₀ + 1 = n₁
⊢ x ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ ⋯ ⋯).g = 0

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.cycles f₁ f₂₃ n₁
hx₂ : x₂ ≫ X.iCycles f₁ f₂₃ n₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0
⊢ (x₂ ≫ X.iCycles f₁ f₂₃ n₁) ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ ⋯ ⋯).g = 0

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ f₁ ≫ f₂₃ = f₁₂ ≫ f₃

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ (𝟙 (mk₁ (f₁₂ ≫ f₃))).app 1 = (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 2

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx✝ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ f₁ ≫ f₂₃ = f₁₂ ≫ f₃

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m n✝ : M
t : R
x : L
f : M →ₗ[R] N
n : M
⊢ ⁅t • x, f⁆ n = (t • ⁅x, f⁆) n

Tactic:
simp only [smul_sub, smul_lie, smul_apply, LieHom.lie_apply, map_smul]

Goal state after:
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m n✝ : M
t : R
x : L
f : M →ₗ[R] N
n : M
⊢ ⁅x, t • f⁆ n = (t • ⁅x, f⁆) n

Tactic:
simp only [smul_sub, smul_apply, LieHom.lie_apply, lie_smul]

Goal state after:
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
x✝² : L₁ ≃ₗ⁅R⁆ L₂
x✝¹ x✝ : L₁
⊢ x✝² (x✝¹ + x✝) = x✝² x✝¹ + x✝² x✝

Tactic:
← coe_toLinearEquiv,

Goal state after:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
x✝² : L₁ ≃ₗ⁅R⁆ L₂
x✝¹ x✝ : L₁
⊢ x✝².toLinearEquiv (x✝¹ + x✝) = x✝².toLinearEquiv x✝¹ + x✝².toLinearEquiv x✝