mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝³ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
inst✝² : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst✝¹ : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
this : HasBinaryCoproduct (((curriedTensor C).obj X₁).obj Y₂) (((curriedTensor C).obj Y₁).obj X₂)
⊢ Cofork.π (c₁.mapBifunctor c₂ (curriedTensor C)) ≫ (Iso.refl (c₁.mapBifunctor c₂ (curriedTensor C)).pt).hom =
    Cofork.π (c₁.tensor c₂)

Tactic:
dsimp only [Cofork.π]; simp [tensorHom_def]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ CommMon D
⊢ (β_ ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X
          ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X).hom ≫
      μ =
    μ

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ CommMon D
X : C
⊢ ((β_ ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X
              ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X).hom ≫
          μ).app
      X =
    μ.app X
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
⊢ o.matrixDecomposition (𝟙 (⨁ fun a ↦ s (f a))) (f b) ⟨b, ⋯⟩ ⟨a, j_property✝⟩ = 1 ⟨b, ⋯⟩ ⟨a, j_property✝⟩

Tactic:
simp only [Category.comp_id, Category.id_comp, End.one_def, eqToHom_refl,
    Matrix.one_apply, HomOrthogonal.matrixDecomposition_apply, biproduct.components]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b =
    if ⟨b, ⋯⟩ = ⟨a, j_property✝⟩ then 𝟙 (s (f b)) else 0
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0

Tactic:
simp only [o.eq_zero nm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ a,
      ∑ s,
        if h : ⟨a, s⟩.fst = j then
          if h_1 : ⋯ ▸ ⟨a, s⟩.snd = x then
            if h_2 : ⟨a, s⟩.fst = j' then if h_3 : ⋯ ▸ ⟨a, s⟩.snd = y then eqToHom ⋯ else 0 else 0
          else 0
        else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
dsimp +instances

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ a,
      ∑ s,
        if h : a = j then
          if h_1 : ⋯ ▸ s = x then if h_2 : a = j' then if h_3 : ⋯ ▸ s = y then eqToHom ⋯ else 0 else 0 else 0
        else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
S : Subtype (J.PropSetWithTop κ')
x✝ : ↑↑S
⊢ x✝ ≤ ⟨⊤, ⋯⟩

Tactic:
Subtype.mk_le_mk

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
S : Subtype (J.PropSetWithTop κ')
x✝ : ↑↑S
⊢ ↑x✝ ≤ ⊤
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
K : Type u
α : K → Subtype (J.PropSetWithTop κ')
hK : HasCardinalLT K κ'
hκ' : Cardinal.aleph0 ≤ κ'
k : K
⊢ α k ≤ ⟨(⋃ k, ↑(α k)) ∪ {⊤}, ⋯⟩

Tactic:
Subtype.mk_le_mk

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
K : Type u
α : K → Subtype (J.PropSetWithTop κ')
hK : HasCardinalLT K κ'
hκ' : Cardinal.aleph0 ≤ κ'
k : K
⊢ ↑(α k) ⊆ (⋃ k, ↑(α k)) ∪ {⊤}
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
⊢ ∀ {i j : J} {f : i ⟶ j}, (D₁.W ⊔ D₂.W) f → (D₁.P ⊔ D₂.P) i

Tactic:
by
    rintro _ _ _ (h | h)
    · exact Or.inl (D₁.src h)
    · exact Or.inr (D₂.src h)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredColimits C κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J W.isLocal.ι

Tactic:
by
    have := W.isClosedUnderColimitsOfShape_isLocal J κ hW
    have := HasCardinalFilteredColimits.hasColimitsOfShape C κ J
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ IsCardinalLocallyPresentable (Type u) κ

Tactic:
IsCardinalLocallyPresentable.iff_exists_isStrongGenerator

Goal state after:
X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Type u) κ
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
this : IsFiltered κ.ord.ToType
x✝¹ : J × κ.ord.ToType
j : J
x : κ.ord.ToType
x✝ : (j, Order.succ x) ⟶ (j, x)
fst✝ : (j, Order.succ x).1 ⟶ (j, x).1
f : (j, Order.succ x).2 ⟶ (j, x).2
⊢ False

Tactic:
have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
        exact not_isMax _ (Order.max_of_succ_le (leOfHom f))

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
X : C
y : (F.obj (op 0)).obj.obj (op X)
n : ℕ
⊢ (coherentTopology C).yoneda.map (limit.π (preimageDiagram hF X y) (op (n + 1))) ≫
      (coherentTopology C).yoneda.map ((preimageDiagram hF X y).map (homOfLE ⋯).op) ≫
        (coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x n) =
    (coherentTopology C).yoneda.map (limit.π (preimageDiagram hF X y) (op (n + 1))) ≫
      (coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x (n + 1)) ≫ F.map (homOfLE ⋯).op

Tactic:
simp [GrothendieckTopology.yonedaEquiv_symm_naturality_left,
      GrothendieckTopology.yonedaEquiv_symm_naturality_right,
      preimageDiagram, (preimageStruct hF X y).w n]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
⊢ (cylinder f g).sieve₀ ≤
    Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun i ↦
        (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
⊢ Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun i ↦
        (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
    (cylinder f g).sieve₀

Tactic:
· rw [PreZeroHypercover.sieve₀, Sieve.generate_le_iff]
    rintro - - ⟨i⟩
    refine ⟨_, 𝟙 _, (cylinder f g).f _, ⟨_, _, ?_⟩, by simp⟩
    simp only [Sieve.pullback_apply, pullback.condition]
    exact Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ _) _

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
⊢ Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun i ↦
        (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
    (cylinder f g).sieve₀
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ (cylinder f g).sieve₁' i j ≤
    Sieve.pullback
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst)

Tactic:
rw [sieve₁', Sieve.ofArrows, Sieve.generate_le_iff]
    rintro - - ⟨k⟩
    refine ⟨E.Y k.down, pullback.snd _ _, E.toPullback k.down, Presieve.ofArrows.mk k.down, ?_⟩
    simp only [cylinder_Y, cylinder_f, toPullback_cylinder, pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (φ.hom i₁)) ≫
        (F.map p.op.toLoc).toFunctor.map (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (φ.hom i₁) ≫ D₂.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ F.map (op f) ≫ (↑s (op X₂)).app (op (Over.mk (𝟙 X₂))) =
    ((Over.forget (unop (op X₁))).op ⋙ F).map (Over.homMk f ⋯).op ≫ (↑s (op X₁)).app (op (Over.mk f))

Tactic:
rw [← s.2 f.op]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ F.map (op f) ≫ ((ConcreteCategory.hom ((presheafHom F G).map f.op)) (↑s (op X₁))).app (op (Over.mk (𝟙 X₂))) =
    ((Over.forget (unop (op X₁))).op ⋙ F).map (Over.homMk f ⋯).op ≫ (↑s (op X₁)).app (op (Over.mk f))
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j j' : Under (op X)
φ : j ⟶ j'
⊢ curry (g.app (op (Over.mk j.hom.unop))) ≫ eHomWhiskerLeft A (F.obj j.right) (G.map (Under.Hom.right φ)) =
    curry (g.app (op (Over.mk j'.hom.unop))) ≫ (pre (F.map (Under.Hom.right φ))).app (G.obj j'.right)

Tactic:
enrichedOrdinaryCategorySelf_eHomWhiskerLeft,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j j' : Under (op X)
φ : j ⟶ j'
⊢ curry (g.app (op (Over.mk j.hom.unop))) ≫ (ihom (F.obj j.right)).map (G.map (Under.Hom.right φ)) =
    curry (g.app (op (Over.mk j'.hom.unop))) ≫ (pre (F.map (Under.Hom.right φ))).app (G.obj j'.right)
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
⊢ ∀ {x y : OneCocycle G U}, x.IsCohomologous y → y.IsCohomologous x

Tactic:
by
    rintro γ₁ γ₂ ⟨α, h⟩
    exact ⟨_, h.symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Types

Goal state before:
pp: α : Type u
f g : MonoOver α
t : f ⟶ g
⊢ Set.range ⇑(hom f.obj.hom) ⊆ Set.range ⇑(hom g.obj.hom)

Tactic:
rintro a ⟨x, rfl⟩

Goal state after:
α : Type u
f g : MonoOver α
t : f ⟶ g
x : f.obj.left
⊢ (hom f.obj.hom) x ∈ Set.range ⇑(hom g.obj.hom)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
⊢ adj.op.CommShift ℤ

Tactic:
eq

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
⊢ (PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)).CommShift ℤ
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
← Functor.map_comp_assoc,

Goal state after:
case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map
        (((shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
          ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).inv.app X).unop ≫
          ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map (((commShiftIso F.op n).hom.app X).unop ≫ ((commShiftIso F.op n).inv.app X).unop) ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
⊢ iso C 0 = Functor.CommShift.isoZero (opOp C) ℤ

Tactic:
ext X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
⊢ (iso C 0).hom.app X = (Functor.CommShift.isoZero (opOp C) ℤ).hom.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
p q : ℤ
⊢ iso C (p + q) = Functor.CommShift.isoAdd (iso C p) (iso C q)

Tactic:
ext X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
p q : ℤ
X : C
⊢ (iso C (p + q)).hom.app X = (Functor.CommShift.isoAdd (iso C p) (iso C q)).hom.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
⊢ iso C 0 = Functor.CommShift.isoZero (unopUnop C) ℤ

Tactic:
ext X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖᵒᵖ
⊢ (iso C 0).hom.app X = (Functor.CommShift.isoZero (unopUnop C) ℤ).hom.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
p q : ℤ
⊢ iso C (p + q) = Functor.CommShift.isoAdd (iso C p) (iso C q)

Tactic:
ext X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
p q : ℤ
X : Cᵒᵖᵒᵖ
⊢ (iso C (p + q)).hom.app X = (Functor.CommShift.isoAdd (iso C p) (iso C q)).hom.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
⊢ (Functor.commShiftIso ((opOpEquivalence C).inverse ⋙ (opOpEquivalence C).functor) n).hom ≫
      Functor.whiskerRight (opOpEquivalence C).counitIso.hom (shiftFunctor C n) =
    (shiftFunctor C n).whiskerLeft (opOpEquivalence C).counitIso.hom ≫ (Functor.commShiftIso (𝟭 C) n).hom

Tactic:
ext X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X : C
⊢ ((Functor.commShiftIso ((opOpEquivalence C).inverse ⋙ (opOpEquivalence C).functor) n).hom ≫
          Functor.whiskerRight (opOpEquivalence C).counitIso.hom (shiftFunctor C n)).app
      X =
    ((shiftFunctor C n).whiskerLeft (opOpEquivalence C).counitIso.hom ≫ (Functor.commShiftIso (𝟭 C) n).hom).app X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
H : Type u'
inst✝¹ : Category.{v', u'} H
inst✝ : Preadditive H
⊢ t.heart.ι.essImage = t.heart

Tactic:
ext X

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
H : Type u'
inst✝¹ : Category.{v', u'} H
inst✝ : Preadditive H
X : C
⊢ t.heart.ι.essImage X ↔ t.heart X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
        (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
          (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
← Functor.map_comp_assoc,

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X ≫ (t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
      (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
        (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))