mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ tensorHom ℬ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom (𝟙 Z) ≫
      (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
        tensorHom ℬ (𝟙 W) (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom =
    (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
      (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom

Tactic:
dsimp [tensorHom]
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩
  · simp
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩
  · simp
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X✝ Y✝ Z : C
inst✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv =
    ((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv

Tactic:
ext <;> simp [← F.map_comp]

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
⊢ lower ((m + n) :: raise l (m + n)) n = m :: l

Tactic:
lower,

Goal state after:
m : ℕ
l : List ℕ
n : ℕ
⊢ (m + n - n) :: lower (raise l (m + n)) (m + n) = m :: l
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ a ∈ ↑(rangeOfWType s)

Tactic:
← Subtype.val_injective.mem_set_image

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ Subtype.val '' ↑(rangeOfWType s)
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
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i

Tactic:
simp_rw [map_smul, LinearMap.smul_apply, toDual_apply, smul_eq_mul, mul_boole,
    Finset.sum_ite_eq', Finsupp.if_mem_support]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : I₁ a • (B x) y = 0
⊢ (B x) y = 0

Tactic:
smul_eq_zero

Goal state after:
case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : I₁ a = 0 ∨ (B x) y = 0
⊢ (B x) y = 0
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
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
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Dual R M ⊗[R] N
⊢ (dualTensorHomEquivOfBasis b).symm ((dualTensorHomEquivOfBasis b) x) = x

Tactic:
LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b

Goal state after:
ι : Type u_1
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
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Dual R M ⊗[R] N
⊢ x = x
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K (Dual K V)
⊢ finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V

Tactic:
finrank_add_finrank_dualAnnihilator_eq,

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K (Dual K V)
⊢ finrank K (Dual K V) = finrank K V
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (CokernelCofork.ofπ h ⋯)

Tactic:
letI hn := regularOfIsPushoutSndOfRegular gn.regularEpi comm t
    have q := (@zero_comp _ _ _ gn.W _ _ f).symm
    convert! hn.isColimit

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
⊢ ∃ f, ∀ i ∈ s, f (v i) = 1

Tactic:
refine ⟨b.constr K 1, fun i hi ↦ ?_⟩

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
i : ι
hi : i ∈ s
⊢ ((b.constr K) 1) (v i) = 1
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ 0 ≫ diag A = 0 ≫ prod.lift (𝟙 A) 0

Tactic:
zero_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ 0 = 0 ≫ prod.lift (𝟙 A) 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = prod.map f f ≫ σ

Tactic:
by rw [← hg, Cofork.π_ofπ, hfg]

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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ f ≫ h - (0 ≫ h - g ≫ h) = f ≫ h + g ≫ h

Tactic:
zero_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ f ≫ h - (0 - g ≫ h) = f ≫ h + g ≫ h
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
⊢ S.f = 0 ≫ h.i

Tactic:
zero_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
⊢ S.f = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
hg : S.g = 0
⊢ (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0 ≫ (ofZeros S hf hg).i

Tactic:
zero_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
hg : S.g = 0
⊢ (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
⊢ h₁.f' ≫ φK ≫ h₂.π = 0

Tactic:
rw [reassoc_of% commf', h₂.f'_π, comp_zero]

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

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

Tactic:
zero_comp,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
⊢ (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
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
e : S₁ ≅ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap (𝟙 S₁) = 𝟙 S₁.opcycles

Tactic:
opcyclesMap_id

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ 𝟙 S₁.opcycles = 𝟙 S₁.opcycles
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
e : S₁ ≅ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap (𝟙 S₂) = 𝟙 S₂.opcycles

Tactic:
opcyclesMap_id

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ 𝟙 S₂.opcycles = 𝟙 S₂.opcycles
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ S₁.homologyπ ≫ homologyMap φ ≫ z = S₁.homologyπ ≫ 𝟙 S₁.homology

Tactic:
homologyπ_naturality_assoc,

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ cyclesMap φ ≫ S₂.homologyπ ≫ z = S₁.homologyπ ≫ 𝟙 S₁.homology
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
    (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Tactic:
← cancel_epi (S₁.mapRightHomologyIso F).hom,

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✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ (S₁.mapRightHomologyIso F).hom ≫ F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ hkf.lift (KernelFork.ofι S.f ⋯) ≫ (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ = 0 ≫ (isoHomology S hkf hcc fac).hom

Tactic:
zero_comp,

Goal state after:
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ hkf.lift (KernelFork.ofι S.f ⋯) ≫ (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ IsColimit (CokernelCofork.ofπ π ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsCokernel

Goal state after:
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0 ≅
    parallelPair S.toCycles 0

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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj (CokernelCofork.ofπ π ⋯) ≅ CokernelCofork.ofπ S.homologyπ ⋯
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₃ = 0

Tactic:
← ψ.comm₂₃_assoc,

Goal state after:
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₃ = 0
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case h.h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.fst = g ≫ prod.fst

Tactic:
simp only [prod.lift_fst]

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

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ S.f = 0 ≫ h.i

Tactic:
zero_comp,

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ S.f = 0
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
⊢ h.g' = 0

Tactic:
rw [← cancel_epi h.p, h.p_g', comp_zero, hg]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
presf : PreservesLimit (parallelPair bc.snd 0) F := inst✝
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))

Tactic:
let hf : IsLimit bc.sndKernelFork := BinaryBicone.isLimitSndKernelFork i

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
presf : PreservesLimit (parallelPair bc.snd 0) F := inst✝
hf : IsLimit bc.sndKernelFork := BinaryBicone.isLimitSndKernelFork i
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ h.left.π ≫ 0 ≫ h.right.ι = 0

Tactic:
zero_comp,

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ h.left.π ≫ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ S.liftCycles a ha ≫ 0 ≫ S.descOpcycles b hb = 0

Tactic:
zero_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ S.liftCycles a ha ≫ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
⊢ S.Exact → Epi S.f

Tactic:
intro h
    have := h.hasHomology
    simp only [exact_iff_isZero_homology] at h
    have := S.isIso_iCycles hg
    have : Epi S.toCycles := epi_of_isZero_cokernel' _ S.homologyIsCokernel h
    rw [← S.toCycles_i]
    apply epi_comp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ S.pOpcycles ≫ S.fromOpcycles = 0 ≫ S.fromOpcycles

Tactic:
zero_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ S.pOpcycles ≫ S.fromOpcycles = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
Z'✝ : C
x : S.X₂ ⟶ Z'✝
hx : S.f ≫ x = 0
⊢ S.g ≫ s.s ≫ x = x

Tactic:
by simp only [s.g_s_assoc, sub_comp, id_comp, sub_eq_self, assoc, hx, comp_zero]

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

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
⊢ g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt

Tactic:
simp [g']

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

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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f - 0 ≫ s = 𝟙 S.X₁ ≫ S.f

Tactic:
zero_comp,

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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f - 0 = 𝟙 S.X₁ ≫ S.f
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
x✝ : Mono f
⊢ kernel.ι f = 0

Tactic:
by rw [← cancel_mono f, kernel.condition, zero_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ F.map (kernel.ι S.g ≫ cokernel.π S.f) = 0

Tactic:
F.map_comp,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ F.map (kernel.ι S.g) ≫ F.map (cokernel.π S.f) = 0