mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y x : C
hx : Q x
r : Retract y x
a : Subtype R
h₁ : Q (X a)
h₂ : g (h a) h₁ = g r hx
⊢ (ofObj Y).isoClosure y

Tactic:
obtain rfl : x = X a := Subtype.ext_iff.1 (congr_arg Sigma.fst h₂.symm)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
⊢ (ofObj Y).isoClosure y
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯ ≫ fst (fst f' g') i₁ =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂

Tactic:
lift_fst,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ = lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ P (pullback.diagonal (e.hom ≫ f))

Tactic:
pullback.diagonal_comp,

Goal state after:
case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ P
    (pullback.diagonal e.hom ≫
      (pullbackDiagonalMapIdIso e.hom e.hom f).inv ≫
        pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
⊢ P (pullback.diagonal (f ≫ e.hom))

Tactic:
pullback.diagonal_comp,

Goal state after:
case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
⊢ P
    (pullback.diagonal f ≫
      (pullbackDiagonalMapIdIso f f e.hom).inv ≫
        pullback.snd (pullback.diagonal e.hom) (pullback.map (f ≫ e.hom) (f ≫ e.hom) e.hom e.hom f f (𝟙 Z) ⋯ ⋯))
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
e : J ≌ J'
inst✝ : P.IsClosedUnderColimitsOfShape J
⊢ P.IsClosedUnderColimitsOfShape J'

Tactic:
rwa [← P.isClosedUnderColimitsOfShape_iff_of_equivalence e]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
⊢ ∀ (i₁ : X' ⟶ X) (i₂ : Z' ⟶ Z) (f' : X' ⟶ Z'), IsPullback f' i₁ i₂ (e.hom ≫ f) → P f'

Tactic:
i₁

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
⊢ ∀ (i₂ : Z' ⟶ Z) (f' : X' ⟶ Z'), IsPullback f' i₁ i₂ (e.hom ≫ f) → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
⊢ ∀ (i₁ : X' ⟶ X) (i₂ : Z' ⟶ Z) (f' : X' ⟶ Z'), IsPullback f' i₁ i₂ (f ≫ e.hom) → P f'

Tactic:
i₁

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
⊢ ∀ (i₂ : Z' ⟶ Z) (f' : X' ⟶ Z'), IsPullback f' i₁ i₂ (f ≫ e.hom) → P f'
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ρ_ ((ihom x).obj y)).inv ≫ (ihom x).obj y ◁ id y ≫ comp x y y = 𝟙 ((ihom x).obj y)

Tactic:
apply uncurry_injective
  rw [uncurry_natural_left, uncurry_natural_left, comp_eq, uncurry_curry, compTranspose_eq,
    associator_inv_naturality_right_assoc, ← rightUnitor_tensor_inv_assoc,
    whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc, ← uncurry_id_eq_ev y y]
  simp only [Functor.id_obj]
  rw [← uncurry_natural_left]
  simp [id_eq, uncurry_id_eq_ev]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
⊢ False

Tactic:
obtain ⟨⟨ιL, bL⟩⟩ := Module.Free.exists_basis (R := Lᵐᵒᵖ) (M := K)

Goal state after:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
⊢ False
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
⊢ ⇑b.dualBasis = b.coord

Tactic:
ext i x
  apply dualBasis_apply

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_2.hdisjoint
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank K (V ⧸ W) = 1
⊢ Disjoint W (K ∙ v)

Tactic:
· exact Submodule.disjoint_span_singleton_of_notMem hv

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : W = ⊤
⊢ finrank K ↥⊤ = finrank K V

Tactic:
finrank_top

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : W = ⊤
⊢ finrank K V = finrank K V
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
⊢ finrank K (V ⧸ q) = finrank K ↥p

Tactic:
by
    rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i : n
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.single i j 1

Tactic:
ext i' j'

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case right
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
φ : M →ₗ[R] N
x✝ : M
⊢ ((lcomp R N g ∘ₗ lcomp R N f) φ) x✝ = (LinearMap.id φ) x✝

Tactic:
exact congr(φ ($eq _))

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
⊢ PreservesColimit K G

Tactic:
let i : P ⟶ I := coequalizer.π s t

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ PreservesColimit K G
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ∀ (j : WalkingParallelPair),
    ((Cone.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCone c)).π.app
        j =
      (Iso.refl
            ((Cone.postcompose
                    (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
                (G.mapCone c)).pt).hom ≫
        (c.map G).π.app j

Tactic:
by rintro (_ | _) <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ∀ (j : WalkingParallelPair),
    ((Cocone.precompose
                    (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
                (G.mapCocone c)).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose
                    (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
                (G.mapCocone c)).pt).hom =
      (c.map G).ι.app j

Tactic:
by rintro (_ | _) <;> cat_disch

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ m ≫ prod.lift (𝟙 A) 0 = (s.ι ≫ prod.fst) ≫ prod.lift (𝟙 A) 0

Tactic:
convert! h

Goal state after:
case e'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ (s.ι ≫ prod.fst) ≫ prod.lift (𝟙 A) 0 = s.ι
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - 0 = a

Tactic:
sub_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a = a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a + -b = a - b

Tactic:
by rw [add_def, neg_neg]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - 0 - (b - c) = a - (b - c)

Tactic:
sub_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - (b - c) = a - (b - c)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{?u.4, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteProducts C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
hf : AbelianStruct f
⊢ Cofork.π hf.cokernelCofork = 0

Tactic:
simp [← cancel_epi f]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (unopMap φ)

Tactic:
← quasiIso_opMap_iff

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (opMap (unopMap φ))
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.homologyπ ≫ S.homologyι = S.iCycles ≫ S.pOpcycles

Tactic:
by
  dsimp only [homologyπ, homologyι]
  simpa only [assoc, S.leftRightHomologyComparison_fac] using S.π_leftRightHomologyComparison_ι

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.π ≫
      (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData ≫
          leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left) ≫
        leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫
          ((S₂.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₂) S₂.homologyData.right S₂.rightHomologyData) ≫
              rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData h₂) ≫
            h₂.ι =
    h₁.i ≫ φ.τ₂ ≫ h₂.p

Tactic:
simp only [assoc, rightHomologyι_naturality', rightHomologyι_naturality'_assoc,
    leftHomologyπ_naturality'_assoc, HomologyData.comm_assoc, p_opcyclesMap'_assoc,
    id_τ₂, p_opcyclesMap', id_comp, cyclesMap'_i_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ opcyclesMap (opMap φ) ≫ S₁.opcyclesOpIso.hom = S₂.opcyclesOpIso.hom ≫ (cyclesMap φ).op

Tactic:
by
  rw [← cancel_epi S₂.op.pOpcycles, p_opcyclesMap_assoc, opMap_τ₂,
    op_pOpcycles_opcyclesOpIso_hom, op_pOpcycles_opcyclesOpIso_hom_assoc, ← op_comp,
    ← op_comp, cyclesMap_i]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (cyclesMap φ).op ≫ S₁.opcyclesOpIso.inv = S₂.opcyclesOpIso.inv ≫ opcyclesMap (opMap φ)

Tactic:
by
  rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
    ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ S₂.g

Tactic:
φ.comm₂₃

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.g ≫ φ.τ₃ = S₁.g ≫ φ.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ S.f ≫ k ≫ α = 0

Tactic:
by rw [reassoc_of% hk, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Tactic:
by
  have γ : RightHomologyMapData φ h₁ h₂ := default
  simp only [γ.opcyclesMap'_eq, γ.neg.opcyclesMap'_eq, RightHomologyMapData.neg_φQ]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (-φ₁).τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + (-φ₂).τ₁

Tactic:
rw [neg_τ₁, neg_τ₁, h.comm₁, neg_add_rev, comp_neg]; abel

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ IsLimit (π₁.mapCone (KernelFork.ofι i ⋯))

Tactic:
apply Abelian.isLimitMapConeOfKernelForkOfι

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ IsLimit (π₂.mapCone (KernelFork.ofι i ⋯))

Tactic:
apply Abelian.isLimitMapConeOfKernelForkOfι

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

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ IsLimit (π₃.mapCone (KernelFork.ofι i ⋯))

Tactic:
apply Abelian.isLimitMapConeOfKernelForkOfι

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₁ = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂ - φ₄).τ₁

Tactic:
rw [sub_τ₁, sub_τ₁, h.comm₁, h'.comm₁, comp_sub]; abel

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

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
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      { τ₁ := colimit.ι (F ⋙ π₁) x✝, τ₂ := colimit.ι (F ⋙ π₂) x✝, τ₃ := colimit.ι (F ⋙ π₃) x✝, comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    { τ₁ := colimit.ι (F ⋙ π₁) x✝¹, τ₂ := colimit.ι (F ⋙ π₂) x✝¹, τ₃ := colimit.ι (F ⋙ π₃) x✝¹, comm₁₂ := ⋯,
        comm₂₃ := ⋯ } ≫
      ((const J).obj
            { X₁ := colimit (F ⋙ π₁), X₂ := colimit (F ⋙ π₂), X₃ := colimit (F ⋙ π₃),
              f := colimMap (F.whiskerLeft π₁Toπ₂), g := colimMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
        f

Tactic:
ext
        · simp [← colimit.w (F ⋙ π₁) f]
        · simp [← colimit.w (F ⋙ π₂) f]
        · simp [← colimit.w (F ⋙ π₃) f]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂

Tactic:
rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
⊢ Epi S₂.g

Tactic:
suffices Epi (e.hom.τ₂ ≫ S₂.g) by
      exact epi_of_epi e.hom.τ₂ _

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
⊢ Epi (e.hom.τ₂ ≫ S₂.g)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S₁ S₂ S₃ S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ 0 - 0 = 0

Tactic:
sub_zero

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S₁ S₂ S₃ S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ 0 = 0