mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ (G.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫ c.ι.app Y.base =
    (G.map ((Grothendieck.ιNatTrans f).app X.fiber) ≫
        colimit.ι (Grothendieck.ι F Y.base ⋙ G) ((F.map f).toFunctor.obj X.fiber)) ≫
      c.ι.app Y.base

Tactic:
rw [← colimit.w _ g, ← Category.assoc, Functor.comp_map, ← G.map_comp]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ (G.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫ c.ι.app Y.base =
    (G.map ((Grothendieck.ιNatTrans f).app X.fiber ≫ (Grothendieck.ι F Y.base).map g) ≫
        colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫
      c.ι.app Y.base
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
hker : (RingHom.ker f.toRingHom).FG
⊢ f.FinitePresentation

Tactic:
by
  -- Porting note: added `convert`
  convert! RingHom.FinitePresentation.of_surjective f hf hker

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

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C
F : C₀ ⥤ C
X : C
inst✝ : F.Initial
Y : Over X
⊢ IsConnected (CostructuredArrow (CostructuredArrow.toOver F X) Y)

Tactic:
by
    rw [isConnected_iff_of_equivalence
      (CostructuredArrow.costructuredArrowToOverEquivalence F Y)]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.pushouts

Tactic:
intro X Y p hp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
p : X ⟶ Y
hp : P p
⊢ P.pushouts p
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), α ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ W α

Tactic:
by
    let φ := fun j => f.app (Discrete.mk j)
    have : HasLimit X₁ := ⟨c₁, hc₁⟩
    have : HasLimit X₂ := ⟨c₂, hc₂⟩
    have : HasProduct fun j ↦ X₁.obj (Discrete.mk j) :=
      hasLimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₁.obj j)))
    have : HasProduct fun j ↦ X₂.obj (Discrete.mk j) :=
      hasLimit_of_iso (Discrete.natIso (fun j ↦ Iso.refl (X₂.obj j)))
    have hf' := hW _ _ φ (fun j => hf (Discrete.mk j))
    refine (W.arrow_mk_iso_iff ?_).2 hf'
    refine Arrow.isoMk
      (IsLimit.conePointUniqueUpToIso hc₁ (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm)
      (IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) ?_
    apply limit.hom_ext
    rintro ⟨j⟩
    simp [φ, hα]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (ρ_ X).hom = fst X (𝟙_ C)

Tactic:
by simp [fst_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (ρ_ X).inv ≫ fst X (𝟙_ C) = 𝟙 X

Tactic:
by simp [fst_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
⊢ i ∈ ⋯.toFinset ↔ (ε i) m ≠ 0

Tactic:
Set.Finite.mem_toFinset,

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
⊢ i ∈ {i | (ε i) m ≠ 0} ↔ (ε i) m ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
e : (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
this : Module.rank R (M' ⧸ Submodule.map f p) = Module.rank R (M' ⧸ f.range) + Module.rank R ↥f'.ker
⊢ Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)

Tactic:
← e.rank_eq

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
e : (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
this :
  Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)
⊢ Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ sec x ∈ span R s

Tactic:
exact Submodule.subset_span hxs

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ #↑s + Module.rank R (M ⧸ span R s) = Module.rank R M

pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec

Tactic:
← rank_quotient_add_rank (Submodule.span R s),

Goal state after:
case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ #↑s + Module.rank R (M ⧸ span R s) = Module.rank R (M ⧸ span R s) + Module.rank R ↥(span R s)

case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr
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₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
hij : i ≠ j
⊢ (B (v i)) (v j) = 0

Tactic:
· exact h hij

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
h : W ⟶ X
t : IsSplitEqualizer f g h
s : Fork f g
⊢ (s.ι ≫ t.leftRetraction) ≫ t.asFork.ι = s.ι

Tactic:
by simp [-top_rightRetraction, ← t.top_rightRetraction, s.condition_assoc]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y z : M
⊢ 0 ≤ (B z) z

Tactic:
obtain rfl | hz := eq_or_ne z 0

Goal state after:
case inl
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
⊢ 0 ≤ (B 0) 0

case inr
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y z : M
hz : z ≠ 0
⊢ 0 ≤ (B z) z
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₁
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
by
  refine le_antisymm ?_ (sup_dualAnnihilator_le_inf W W')
  let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (Submodule.mkQ W).prod (Submodule.mkQ W')
  have : LinearMap.ker F = W ⊓ W' := by simp only [F, LinearMap.ker_prod, ker_mkQ]
  rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]
  intro φ
  rw [LinearMap.mem_range]
  rintro ⟨x, rfl⟩
  rw [Submodule.mem_sup]
  obtain ⟨⟨a, b⟩, rfl⟩ := (dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')).surjective x
  obtain ⟨a', rfl⟩ := (dualQuotEquivDualAnnihilator W).symm.surjective a
  obtain ⟨b', rfl⟩ := (dualQuotEquivDualAnnihilator W').symm.surjective b
  use a', a'.property, b', b'.property
  rfl

Goal state after:
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
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ ∀ (j : WalkingParallelPair),
    m'.unop ≫ (KernelFork.ofι f.unop ⋯).π.app j = (KernelFork.ofι (m'.unop ≫ f.unop) ⋯).π.app j

Tactic:
rintro (⟨⟩ | ⟨⟩)

Goal state after:
case zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop ≫ (KernelFork.ofι f.unop ⋯).π.app WalkingParallelPair.zero =
    (KernelFork.ofι (m'.unop ≫ f.unop) ⋯).π.app WalkingParallelPair.zero

case one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop ≫ (KernelFork.ofι f.unop ⋯).π.app WalkingParallelPair.one =
    (KernelFork.ofι (m'.unop ≫ f.unop) ⋯).π.app WalkingParallelPair.one
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
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ ∀ (j : WalkingParallelPair),
    (CokernelCofork.ofπ f.unop ⋯).ι.app j ≫ m'.unop = (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯).ι.app j

Tactic:
rintro (⟨⟩ | ⟨⟩)

Goal state after:
case zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ (CokernelCofork.ofπ f.unop ⋯).ι.app WalkingParallelPair.zero ≫ m'.unop =
    (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯).ι.app WalkingParallelPair.zero

case one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ (CokernelCofork.ofπ f.unop ⋯).ι.app WalkingParallelPair.one ≫ m'.unop =
    (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯).ι.app WalkingParallelPair.one
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.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
⊢ g = 0

Tactic:
have hf : h ≫ f = 0 :=
      calc
        h ≫ f = h ≫ p ≫ i := (Abelian.coimage.fac f).symm ▸ rfl
        _ = h ≫ p ≫ cokernel.π g ≫ t := ht ▸ rfl
        _ = h ≫ u ≫ t := by simp only [u, Category.assoc]
        _ = 0 ≫ t := by rw [← Category.assoc, hu.w]
        _ = 0 := zero_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
hf : h ≫ f = 0
⊢ g = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ diag X ≫ σ = 0

Tactic:
cokernel.condition_assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ 0 ≫ inv (r X) = 0
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.HasLeftHomology
inst✝ : S.HasRightHomology
h : IsIso S.leftRightHomologyComparison
⊢ S.HasHomology

Tactic:
have : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData) := h
  exact hasHomology_of_isIso_leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData

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 : ShortComplex C
inst✝ : S.HasHomology
⊢ S.toCycles ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom = 0

Tactic:
simp only [toCycles_comp_leftHomologyπ_assoc, zero_comp]

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

Goal state before:
pp: case refine_2
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π ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology

Tactic:
reassoc_of% hz,

Goal state after:
case refine_2
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π
⊢ inv (cyclesMap φ) ≫ S₁.homologyπ ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_2
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 φ)
⊢ z ≫ S₁.homologyι ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι

Tactic:
reassoc_of% hz,

Goal state after:
case refine_2
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 φ)
⊢ S₂.homologyι ≫ inv (opcyclesMap φ) ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι
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
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } ≫
      c.π.app j =
    s.π.app j

Tactic:
ext <;> apply IsLimit.fac

Goal state after:
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
⊢ S.RightHomologyData

Tactic:
by
  let γ := kernel.ι S.g ≫ cokernel.π S.f
  let g' := cokernel.desc S.f S.g S.zero
  have hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' (by simp [γ, g']) := by rw [cokernel.π_desc]
  have wι : kernel.ι (cokernel.π γ) ≫ g' = 0 := by rw [hg', kernel.condition_assoc, zero_comp]
  let e : cokernel γ ≅ Abelian.coimage S.g :=
    IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) S.cokernelToAbelianCoimageIsCokernel
  have he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage :=
    IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one
  have fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g := by
    rw [hg', reassoc_of% he]
    simp only [γ, g', cokernel.π_desc, ← cancel_epi (cokernel.π S.f),
      cokernel_π_comp_cokernelToAbelianCoimage_assoc]
  have hι : IsLimit (KernelFork.ofι _ wι) :=
    KernelFork.IsLimit.ofι _ _
      (fun x hx => kernel.lift _ x (by
        simpa only [← cancel_mono e.hom, ← cancel_mono (Abelian.factorThruCoimage S.g), assoc,
          zero_comp, fac] using hx))
      (fun x hx => kernel.lift_ι _ _ _)
      (fun x hx b hb => equalizer.hom_ext (by simp only [hb, kernel.lift_ι]))
  exact
    { Q := cokernel S.f,
      H := Abelian.image (kernel.ι S.g ≫ cokernel.π S.f)
      p := cokernel.π _
      ι := kernel.ι _
      wp := cokernel.condition _
      hp := cokernelIsCokernel _
      wι := wι
      hι := hι }

Goal state after:
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₂

Tactic:
intro h x₂ hx₂

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

Goal state before:
pp: case mp
S : ShortComplex Ab
x₂ : ↑S.X₂
h : (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
⊢ (ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)

Tactic:
refine ⟨h, ?_⟩

Goal state after:
case mp
S : ShortComplex Ab
x₂ : ↑S.X₂
h : (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
⊢ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f) → (ConcreteCategory.hom S.g) x₂ = 0
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✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ S.Exact ↔ Epi (kernel.lift S.g S.f ⋯)

Tactic:
rw [exact_iff_epi_toCycles]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ Epi S.toCycles ↔ Epi (kernel.lift S.g S.f ⋯)
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 : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ S.Exact

Tactic:
rw [exact_iff_epi_toCycles]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ Epi S.toCycles
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 S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂

Tactic:
rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]

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

Goal state before:
pp: case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ S₂.liftCycles φ.τ₂ ⋯ ≫ S₂.iCycles = 𝟙 S₁.X₂ ≫ φ.τ₂

Tactic:
liftCycles_i,

Goal state after:
case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂