mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case h₁
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ i ∉ vi.support → (RingHom.id R) (vi i) • (B (v i)) (v i) = 0

Tactic:
intro hi
    replace hi : vi i = 0 := Finsupp.notMem_support_iff.mp hi
    rw [hi, RingHom.id_apply, zero_smul]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ coimageImageComparison f = coimageImageComparison' f

Tactic:
by
  ext
  simp [coimageImageComparison, coimageImageComparison']

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J G

Tactic:
intro J

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
⊢ ∀ [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J G
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
⊢ g = 0

Tactic:
let u := kernel.ι g ≫ i
  have hu := normalMonoOfMono u
  let h := hu.g
  -- By hypothesis, p factors through the kernel of g via some t.
  obtain ⟨t, ht⟩ := kernel.lift' g p hpg
  have fh : f ≫ h = 0 :=
    calc
      f ≫ h = (p ≫ i) ≫ h := (Abelian.image.fac f).symm ▸ rfl
      _ = ((t ≫ kernel.ι g) ≫ i) ≫ h := ht ▸ rfl
      _ = t ≫ u ≫ h := by simp only [u, Category.assoc]
      _ = t ≫ 0 := hu.w ▸ rfl
      _ = 0 := HasZeroMorphisms.comp_zero _ _
  -- h factors through the cokernel of f via some l.
  obtain ⟨l, hl⟩ := cokernel.desc' f h fh
  have hih : i ≫ h = 0 :=
    calc
      i ≫ h = i ≫ cokernel.π f ≫ l := hl ▸ rfl
      _ = 0 ≫ l := by rw [← Category.assoc, kernel.condition]
      _ = 0 := zero_comp
  -- i factors through u = ker h via some s.
  obtain ⟨s, hs⟩ := NormalMono.lift' u i hih
  have hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i := by rw [Category.assoc, hs, Category.id_comp]
  have : Epi (kernel.ι g) := epi_of_epi_fac ((cancel_mono _).1 hs')
  -- ker g is an epimorphism, but ker g ≫ g = 0 = ker g ≫ 0, so g = 0 as required.
  exact zero_of_epi_comp _ (kernel.condition g)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : a ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
⊢ a ≫ a' = b ≫ b'

Tactic:
ha',

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : a ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
⊢ cokernel.π (coprod.desc f g) = b ≫ b'
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_2
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
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f ⋯).pt
hg : g ≫ f = Fork.ι A
⊢ g = limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e

Tactic:
← cancel_mono f,

Goal state after:
case refine_2
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
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f ⋯).pt
hg : g ≫ f = Fork.ι A
⊢ g ≫ f = (limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫ f
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case pos
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

pp: case neg
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
· rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
        change fromCoset _ = fromCoset ⟨f a • (y • _), _⟩
        simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]

Goal state after:
case neg
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩
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
inst✝ : S.HasRightHomology
hf : S.f = 0
this : IsIso S.pOpcycles
⊢ S.opcycles ≅ S.X₂

Tactic:
exact (asIso S.pOpcycles).symm

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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ S₂.leftHomologyData.homologyIso.hom ≫ S₂.leftHomologyData.homologyIso.inv ≫ h₂.homologyIso.hom =
    S₁.leftHomologyData.homologyIso.hom ≫
      S₁.leftHomologyData.homologyIso.inv ≫ h₁.homologyIso.hom ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
Iso.hom_inv_id_assoc,

Goal state after:
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ h₂.homologyIso.hom =
    S₁.leftHomologyData.homologyIso.hom ≫
      S₁.leftHomologyData.homologyIso.inv ≫ h₁.homologyIso.hom ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ h₂.homologyIso.hom =
    S₁.leftHomologyData.homologyIso.hom ≫
      S₁.leftHomologyData.homologyIso.inv ≫ h₁.homologyIso.hom ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
Iso.hom_inv_id_assoc,

Goal state after:
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom
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
h : S.LeftHomologyData
⊢ h.π ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = h.cyclesIso.inv ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, π_comp_leftHomologyIso_inv_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 : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.op.p ≫ S.leftHomologyData.f'.op = S.op.g

Tactic:
LeftHomologyData.op_p,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.i.op ≫ S.leftHomologyData.f'.op = S.op.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₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ S₂.opcyclesOpIso.hom ≫ (cyclesMap φ).op ≫ S₁.opcyclesOpIso.inv =
    S₂.opcyclesOpIso.hom ≫ S₂.opcyclesOpIso.inv ≫ opcyclesMap (opMap φ)

Tactic:
Iso.hom_inv_id_assoc,

Goal state after:
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
⊢ S₂.opcyclesOpIso.hom ≫ (cyclesMap φ).op ≫ S₁.opcyclesOpIso.inv = opcyclesMap (opMap φ)
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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0

Tactic:
rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]

Goal state after:
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 (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology

Tactic:
← cancel_mono S₁.homologyι,

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 (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 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₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
wi : F.map h.i ≫ F.map S.g = 0
hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)
f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)
hf' : f' = F.map h.f'
wπ : f' ≫ F.map h.π = 0
e : parallelPair f' 0 ≅ parallelPair (F.map h.f') 0 :=
  parallelPair.ext (Iso.refl ((parallelPair f' 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair f' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ (CokernelCofork.ofπ h.π ⋯).map F ≅ (Cocone.precompose e.inv).obj (CokernelCofork.ofπ (F.map h.π) wπ)

Tactic:
exact Cofork.ext (Iso.refl _) (by simp [e])

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
S S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : h₁.IsPreservedBy F
inst✝ : h₂.IsPreservedBy F
⊢ (h₁.map F).p ≫ F.map ψ.φQ = (F.mapShortComplex.map φ).τ₂ ≫ (h₂.map F).p

Tactic:
simpa only [F.map_comp] using! F.congr_map ψ.commp

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:
h₁₂.comm₁,

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 φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ S₁.f ≫ h₁₂.h₁ + h₁₂.h₀ + φ₂.τ₁ = S₁.f ≫ (h₁₂.h₁ + h₂₃.h₁) + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mp
S : ShortComplex Ab
⊢ Function.Surjective ⇑S.abToCycles →
    ∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

pp: case mpr
S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    Function.Surjective ⇑S.abToCycles

Tactic:
· intro h x₂ hx₂
    obtain ⟨x₁, hx₁⟩ := h ⟨x₂, hx₂⟩
    exact ⟨x₁, by simpa only [Subtype.ext_iff, abToCycles_apply_coe] using hx₁⟩

Goal state after:
case mpr
S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    Function.Surjective ⇑S.abToCycles
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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

Tactic:
intro eq

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
eq : h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
⊢ IsZero h.left.H
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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact

Tactic:
S.rightHomologyData.exact_iff,

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 : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : IsZero S.rightHomologyData.H
⊢ (S.map F).Exact
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
a : MonoOver X
⊢ p (Quotient.mk'' a)

Tactic:
| _ a
   => 

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
a : MonoOver X
⊢ p (Quotient.mk'' a)
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
inst✝¹ : Balanced C
hS : S.Exact
h : S.RightHomologyData
inst✝ : Epi S.g
⊢ IsIso h.g'

Tactic:
have := hS.mono_g' h
  have := epi_of_epi_fac h.p_g'
  exact isIso_of_mono_of_epi h.g'

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

Tactic:
exact ⟨hS.fIsKernel⟩

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
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ Over.Hom.left e.hom ≫ h.arrow = g.arrow

Tactic:
← cancel_mono f,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ (Over.Hom.left e.hom ≫ h.arrow) ≫ f = g.arrow ≫ 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
F : C ⥤ D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Mono f
⊢ Mono (F.map f)

Tactic:
let S := ShortComplex.mk (0 : X ⟶ X) f 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
F : C ⥤ D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Mono f
S : ShortComplex C := { X₁ := X, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }
⊢ Mono (F.map 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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃

Tactic:
by
    rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobject 0).arrow = 0

Tactic:
by
  rw [← imageSubobject_arrow]
  simp

Goal state after:
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:
← cancel_mono f,

Goal state after:
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 ≫ f = 0 ≫ f
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
⊢ ∀ i ∈ s, (P i).Factors (s.inf P).arrow

Tactic:
induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m

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

Goal state before:
pp: case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          { I := underlying.obj f, m := f.arrow, m_mono := ⋯,
            e := Sigma.desc fun b ↦ Subtype.casesOn b fun g m ↦ underlying.map (homOfLE ⋯), fac := ⋯ }) ≫
      f.arrow =
    (sSup s).arrow

Tactic:
dsimp [sSup]
    rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
⊢ m =
    limit.lift (liftToFinsetObj F)
      { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } }

Tactic:
apply limit.hom_ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
⊢ ∀ (j : (Finset (Discrete α))ᵒᵖ),
    m ≫ limit.π (liftToFinsetObj F) j =
      limit.lift (liftToFinsetObj F)
          { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
        limit.π (liftToFinsetObj F) j