mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Φ : Preradical C
X : C
⊢ Φ.r.map (Φ.ι.app X) ≫ Φ.ι.app X = Φ.ι.app (Φ.r.obj X) ≫ Φ.ι.app X

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Φ : Preradical C
X : C
⊢ Φ.r.map (Φ.ι.app X) ≫ Φ.ι.app X = Φ.ι.app (Φ.r.obj X) ≫ Φ.ι.app X
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
inst✝ : Φ.IsIdempotent
X : C
⊢ IsIso (Φ.ι.app (Φ.r.obj X))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
inst✝ : Φ.IsIdempotent
X : C
⊢ IsIso (Φ.ι.app (Φ.r.obj X))
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
⊢ ∀ (k : D), Mono ((F.whiskerLeft Φ.ι).app k)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
⊢ ∀ (k : D), Mono ((F.whiskerLeft Φ.ι).app k)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
⊢ Module.Injective (End G)ᵐᵒᵖ ↑((preadditiveCoyonedaObj G).1 B)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
⊢ Module.Injective (End G)ᵐᵒᵖ ↑((preadditiveCoyonedaObj G).1 B)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback

Tactic:
]

Goal state after:
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ Function.Injective
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }))

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ Function.Injective
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }))
Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Preradical C
⊢ IsZero (Φ.quotient ⋙ Φ.r) ↔ IsZero (Φ.quotient ⋙ Φ.r)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Radical C
⊢ IsIso (Φ.obj.toColon Φ.obj)

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Radical C
⊢ IsIso (Φ.obj.toColon Φ.obj)
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ ((HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat ⋯).hom ≫
        R.π.f 0 ≫
          (HomologicalComplex.extendXIso ((ChainComplex.single₀ C).obj X) ComplexShape.embeddingDownNat ⋯).inv) ≫
      (((HomologicalComplex.single C (ComplexShape.down ℕ) 0).obj X).extendXIso ComplexShape.embeddingDownNat
            π'._proof_1).hom ≫
        (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X).hom ≫
          (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ ((HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat ⋯).hom ≫
        R.π.f 0 ≫
          (HomologicalComplex.extendXIso ((ChainComplex.single₀ C).obj X) ComplexShape.embeddingDownNat ⋯).inv) ≫
      (((HomologicalComplex.single C (ComplexShape.down ℕ) 0).obj X).extendXIso ComplexShape.embeddingDownNat
            π'._proof_1).hom ≫
        (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X).hom ≫
          (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ Φ.obj.hom.app X = Φ.ι.app X

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ QuasiIso R.ι'

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ QuasiIso R.ι'
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
I : InjectiveResolution Y
J : InjectiveResolution Z
g h : I.cocomplex ⟶ J.cocomplex
g_comm : I.ι ≫ g = (CochainComplex.single₀ C).map f ≫ J.ι
h_comm : I.ι ≫ h = (CochainComplex.single₀ C).map f ≫ J.ι
⊢ I.ι ≫ (g - h) = 0

Tactic:
simp [g_comm, h_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X) ↔ IsZero (Ψ.r.obj (Φ.quotient.obj X))

Tactic:
by
  constructor <;> intro h
  · exact IsZero.of_epi_eq_zero ((colonπ Φ Ψ).app X)
      (zero_of_epi_comp ((toColon Φ Ψ).hom.left.app X) (by simp))
  · obtain ⟨inv, hinv⟩ :=
      KernelFork.IsLimit.lift' (Φ.isLimitKernelForkObj X) ((colon Φ Ψ).ι.app X) (by
        rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp])
    dsimp at hinv
    refine ⟨inv, ?_, ?_⟩
    · simp [← cancel_mono (Φ.ι.app X), hinv]
    · simp [← cancel_mono ((Φ.colon Ψ).ι.app X), hinv]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (𝟙 (injectiveResolution X).cocomplex)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (𝟙 (injectiveResolution X).cocomplex)
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z✝) (injectiveResolution X✝)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc f (injectiveResolution Y✝) (injectiveResolution X✝) ≫
        InjectiveResolution.desc g (injectiveResolution Z✝) (injectiveResolution Y✝))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z✝) (injectiveResolution X✝)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc f (injectiveResolution Y✝) (injectiveResolution X✝) ≫
        InjectiveResolution.desc g (injectiveResolution Z✝) (injectiveResolution Y✝))
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ = (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯ +
          Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) +
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯ +
          Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } :=
  { τ₁ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁,
    τ₂ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂,
    τ₃ := ι { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.Exact

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } :=
  { τ₁ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁,
    τ₂ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂,
    τ₃ := ι { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1)).Exact

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1)).Exact
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯ -
          Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯ -
          Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (-Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (-Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      g ≫ (R.cochainComplexXIso (↑p) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n) n ⋯).inv =
        f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ↔
    ∃ g, g ≫ R.cocomplex.d p n = f

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      g ≫ (R.cochainComplexXIso (↑p) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n) n ⋯).inv =
        f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ↔
    ∃ g, g ≫ R.cocomplex.d p n = f
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ pullback.snd q p' ≫ q' ≫ h.hom = pullback.snd q p' ≫ q' ≫ h.hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt (ofCocomplex Z) (n✝ + 1)

pp: case succ.hK
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((CochainComplex.single₀ C).obj Z) (n✝ + 1)

Tactic:
]

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt (ofCocomplex Z) (n✝ + 1)

case succ.hK
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((CochainComplex.single₀ C).obj Z) (n✝ + 1)
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
a b : Over P
x✝ : a ≈ b
R : C
p : R ⟶ a.left
q : R ⟶ b.left
ep : Epi p
Eq : Epi q
comm : p ≫ a.hom = q ≫ b.hom
⊢ q ≫ b.hom ≫ f = q ≫ b.hom ≫ f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk ((x.hom ≫ f) ≫ g) ≈ Over.mk ((x.hom ≫ f) ≫ g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ ⟦Over.mk ((Over.mk 0).hom ≫ f)⟧ = 0

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ ⟦Over.mk ((Over.mk 0).hom ≫ f)⟧ = 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ ⟦Over.mk (a'.hom ≫ 0)⟧ = ⟦Over.mk 0⟧

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ ⟦Over.mk (a'.hom ≫ 0)⟧ = ⟦Over.mk 0⟧
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ pullback.fst f q.hom ≫ f = pullback.fst f q.hom ≫ f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
p : Over P
hpbar : pseudoApply f ⟦p⟧ = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
hp : ⟦p⟧ = pbar
⊢ ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
p : Over P
hpbar : pseudoApply f ⟦p⟧ = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
hp : ⟦p⟧ = pbar
⊢ ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧