mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)

Tactic:
finrank_top,

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K V₁ ≤ finrank K ↥(LinearMap.ker f ⊔ p)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
⊢ f = g

Tactic:
have hpf : Disjoint (LinearMap.ker f) p := by
    rw [disjoint_iff, Submodule.eq_bot_iff]
    rintro y ⟨hfy : f y = 0, hpy : y ∈ p⟩
    obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hpy
    have ht : t = 0 := by simpa [hx] using hfy
    simp [ht]

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
⊢ f = g
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₁
ι : Type u_4
inst✝ : Finite ι
W : ι → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
revert ι
  apply Finite.induction_empty_option
  · intro α β h hyp W
    rw [← h.iInf_comp, hyp _, ← h.iSup_comp]
  · intro W
    rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]
  · intro α _ h W
    rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]

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 := ⋯
Q : C := ⋯
s : Q ⟶ P := ⋯
t : Q ⟶ P := ⋯
I : C := ⋯
i : P ⟶ I := ⋯
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    (Cofan.mk (G.obj Q) fun j ↦ G.map (Sigma.ι (fun j ↦ K.obj j.fst.1) j)).ι.app { as := f } ≫ G.map s =
      (K ⋙ G).map f.snd ≫ (Cofan.mk (G.obj (∐ K.obj)) fun f ↦ G.map (Sigma.ι K.obj f)).ι.app { as := f.fst.2 }

Tactic:
intro f
      dsimp [P, Q, s, Cofan.mk]
      simp only [← G.map_comp, colimit.ι_desc]
      congr

Goal state after:
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) ⋯) := ⋯
⊢ ∀ (Z : C) (g : Z ⟶ A), g ≫ r A = 0 → g = 0

Tactic:
intro Z x hx

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
⊢ x = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : KernelFork (cokernel.π f)
⊢ (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
    Fork.ι s

Tactic:
simp only [KernelFork.ι_ofι, Category.assoc]
          convert! limit.lift_π s WalkingParallelPair.zero using 2
          rw [IsIso.inv_comp_eq, eq_comm]
          exact (imageMonoFactorisation f).fac

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ factorThruImage f ≫ (coimageIsoImage' f).inv = cokernel.π (kernel.ι f)

Tactic:
simp only [IsImage.isoExt_inv, image.isImage_lift, image.fac_lift,
    coimageStrongEpiMonoFactorisation_e]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m = pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯

Tactic:
apply pullback.hom_ext

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.fst f g = pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullback.fst f g

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.snd f g = pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullback.snd f g
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
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
⊢ IsIso h.π

Tactic:
exact ⟨φ, hφ, by rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]⟩

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
e : S₁ ≅ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap e.inv ≫ leftHomologyMap e.hom = 𝟙 S₂.leftHomology

Tactic:
rw [← leftHomologyMap_comp, e.inv_hom_id, leftHomologyMap_id]

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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
⊢ S₂.LeftHomologyData

Tactic:
let f' := hi.lift (KernelFork.ofι S₂.f S₂.zero)

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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
⊢ S₂.LeftHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftRightHomologyComparison' h₁ h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Tactic:
leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'
    S.homologyData h₁ h₂

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    h₁.homologyIso.inv ≫ h₂.homologyIso.hom
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₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq,
    RightHomologyMapData.comp_φH]

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₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap e.inv ≫ rightHomologyMap e.hom = 𝟙 S₂.rightHomology

Tactic:
rw [← rightHomologyMap_comp, e.inv_hom_id, rightHomologyMap_id]

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₀ + (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁)

Tactic:
abel

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₁.g ≫ h.h₂ + -h.h₁ ≫ S₂.f + (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂)

Tactic:
abel

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.h₃ + -h.h₂ ≫ S₂.g + (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃)

Tactic:
abel

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₀) = -S₁.f ≫ h.h₁ + -h.h₀ + -φ₂.τ₁

Tactic:
abel

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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) = -S₁.g ≫ h.h₂ + -h.h₁ ≫ S₂.f + -φ₂.τ₂

Tactic:
abel

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.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = -h.h₃ + -h.h₂ ≫ S₂.g + -φ₂.τ₃

Tactic:
abel

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₀ + (S₁.f ≫ h₂₃.h₁ + h₂₃.h₀ + φ₃.τ₁) = S₁.f ≫ h₁₂.h₁ + S₁.f ≫ h₂₃.h₁ + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁

Tactic:
abel

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₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
    S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ ≫ S₂.f + h₂₃.h₁ ≫ S₂.f) + φ₃.τ₂

Tactic:
abel

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 φ₂ φ₃
⊢ h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ ≫ S₂.g + h₂₃.h₂ ≫ S₂.g) + φ₃.τ₃

Tactic:
abel

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₀ + φ₂.τ₁ + (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
    S₁.f ≫ h.h₁ + S₁.f ≫ h'.h₁ + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)

Tactic:
abel

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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ + S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f + h'.h₁ ≫ S₂.f) + (φ₂.τ₂ + φ₄.τ₂)

Tactic:
abel

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 φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ + h'.h₃ + (h.h₂ ≫ S₂.g + h'.h₂ ≫ S₂.g) + (φ₂.τ₃ + φ₄.τ₃)

Tactic:
abel

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₀ + φ₂.τ₁ - (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
    S₁.f ≫ h.h₁ - S₁.f ≫ h'.h₁ + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)

Tactic:
abel

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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f - h'.h₁ ≫ S₂.f) + (φ₂.τ₂ - φ₄.τ₂)

Tactic:
abel

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 φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ - h'.h₃ + (h.h₂ ≫ S₂.g - h'.h₂ ≫ S₂.g) + (φ₂.τ₃ - φ₄.τ₃)

Tactic:
abel

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.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃

Tactic:
abel

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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂

Tactic:
abel

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₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁

Tactic:
abel

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₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃

Tactic:
abel

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₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂

Tactic:
abel

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₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁

Tactic:
abel

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

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

Tactic:
abel

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

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

Tactic:
abel

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

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

Tactic:
abel

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₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀

Tactic:
abel

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₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f

Tactic:
abel

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₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₂ ≫ S₂.g + h₃ = h₃ + h₂ ≫ S₂.g

Tactic:
abel

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₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ S₂.f + S₁.f ≫ h₁ ≫ S₂.f

Tactic:
right_eq_add,

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₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₀ ≫ S₂.f = 0
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 : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ S.liftCycles k hk + S.liftCycles k' hk' = S.liftCycles (k + k') ⋯

Tactic:
by
  simp only [← cancel_mono S.iCycles, liftCycles_i, add_comp]

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

Goal state before:
pp: S : ShortComplex Ab
x : ↑S.X₁
⊢ (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x) = 0

Tactic:
rw [← ConcreteCategory.comp_apply, S.zero]

Goal state after:
S : ShortComplex Ab
x : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom (S.abLeftHomologyData.cyclesIso.inv ≫ S.iCycles)) x = ↑x

Tactic:
S.abLeftHomologyData.cyclesIso_inv_comp_iCycles

Goal state after:
S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.abLeftHomologyData.i) x = ↑x
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
h : S.Splitting
⊢ S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s

Tactic:
abel

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
S : ShortComplex Cᵒᵖ
h : S.Splitting
⊢ S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s

Tactic:
abel

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✝¹ : Balanced C
hS : S.Exact
inst✝ : Mono S.f
⊢ IsLimit (KernelFork.ofι S.f ⋯)

Tactic:
by
  have := hS.hasHomology
  have := hS.isIso_toCycles
  exact IsLimit.ofIsoLimit S.cyclesIsKernel
    (Fork.ext (asIso S.toCycles).symm (by simp))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
⊢ ∀ (a b : f ⟶ g), a = b

Tactic:
intro h₁

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ : f ⟶ g
⊢ ∀ (b : f ⟶ g), h₁ = b
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst✝ : HasPullbacks C
y : Subobject Y
h : W ⟶ X
hf : ((Subobject.pullback f).obj y).Factors h
⊢ y.Factors (h ≫ f)

Tactic:
rw [factors_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst✝ : HasPullbacks C
y : Subobject Y
h : W ⟶ X
hf : ((Subobject.pullback f).obj y).Factors h
⊢ (representative.obj y).Factors (h ≫ f)
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✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
⊢ P ⟶ S.X₁

Tactic:
by
  have := hS.epi_toCycles
  exact Projective.factorThru (S.liftCycles f hf) S.toCycles

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.fst =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.fst

Tactic:
· simp only
      apply Quiver.Hom.op_inj
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.snd =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.snd

Tactic:
· simp only
      apply Quiver.Hom.op_inj
      simp

Goal state after: