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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
⊢ Nonempty (P (StructuredArrow.mk (g ≫ Final.homToLift F Y)))

Tactic:
refine isPreconnected_induction P ?_ ?_ h₀ _

Goal state after:
case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
⊢ ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₁ → P j₂

case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
⊢ ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₂ → P j₁
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 ↦ K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x ↦
    match x with
    | { as := as } => Iso.refl ((Discrete.functor fun n_1 ↦ K.obj { as := n_1 }).obj { as := as })
⊢ HasLimit (Discrete.functor fun n_1 ↦ K.obj { as := n_1 })

Tactic:
apply hasProduct_fin

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.isoClosure.colimitsOfShape J = P.colimitsOfShape J

Tactic:
refine le_antisymm ?_ (colimitsOfShape_monotone _ (P.le_isoClosure))
  intro X ⟨h⟩
  choose obj h₁ h₂ using h.prop_diag_obj
  exact
   ⟨{ toColimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
      prop_diag_obj := h₁ }⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P f'

Tactic:
← h.isoPullback_hom_fst,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P (h.isoPullback.hom ≫ pullback.fst i₂ g)
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
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ μ F X Y ≫ α.app (X ⊗ Y) = (α.app X ⊗ₘ α.app Y) ≫ μ G X Y

Tactic:
rw [← cancel_mono (Functor.Monoidal.μIso _ _ _).inv]
    rw [← cancel_epi (Functor.Monoidal.μIso _ _ _).inv]
    apply CartesianMonoidalCategory.hom_ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift f (g ≫ ι) ≫ μ = h ↔ f = lift h g ≫ μ

Tactic:
rw [eq_comm, eq_lift_inv_right, eq_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

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
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
⊢ F.essImage G.X → F.mapGrp.essImage G

Tactic:
rintro ⟨H, ⟨e⟩⟩
    let : GrpObj (F.obj H) := .ofIso e.symm
    let : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
    refine ⟨⟨H⟩, ⟨Grp.mkIso e ?_ ?_⟩⟩ <;> simp

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

Goal state before:
pp: l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2) (m :: raise' l n)

Tactic:
unfold raise'

Goal state after:
l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2)
    (m ::
      match l, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
⊢ Injective ⇑(Dual.eval R M)

Tactic:
intro m m' eq

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq : (Dual.eval R M) m = (Dual.eval R M) m'
⊢ m = m'
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
⊢ 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:
have := f'.rank_eq_of_surjective <| factor_surjective map_le_range

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'.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)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
h : ⊥ = ⊤
⊢ False

Tactic:
cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)

Goal state after:
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
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective ⇑(finsuppLinearMap R)

Tactic:
cases fin

Goal state after:
case inl
ι : 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
h : Function.Bijective ⇑(dualTensorHom R M N)
h✝ : Finite ι
⊢ Function.Bijective ⇑(finsuppLinearMap R)

case inr
ι : 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
h : Function.Bijective ⇑(dualTensorHom R M N)
h✝ : Module.Finite R M
⊢ Function.Bijective ⇑(finsuppLinearMap R)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor (RingHom.id R) M P Q

Tactic:
let e := congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
  have h : Function.Surjective e.toLinearMap := e.surjective
  refine (cancel_right h).1 ?_
  ext f p q m
  simp [e, rTensorHomEquivHomRTensor, smul_tmul']

Goal state after:
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
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(comap (Dual.eval K V) (dualAnnihilator Φ)) = finrank K ↥(dualAnnihilator Φ)

Tactic:
← Module.evalEquiv_toLinearMap

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
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(comap (↑(evalEquiv K V)) (dualAnnihilator Φ)) = finrank K ↥(dualAnnihilator Φ)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f

Tactic:
← LinearMap.range_eq_top,

Goal state after:
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ f.dualMap.range = ⊤ ↔ Function.Injective ⇑f
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ biprod.lift f (-g) ≫ s.π = 0

Tactic:
Cofork.condition s,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ 0 ≫ s.π = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₁ ≫ F.map Y✝.f = F.map X✝.f ≫ F.map φ.τ₂

Tactic:
simp only [← F.map_comp, φ.comm₁₂]

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
⊢ cyclesMap e.inv ≫ cyclesMap e.hom = 𝟙 S₂.cycles

Tactic:
by rw [← cyclesMap_comp, e.inv_hom_id, cyclesMap_id]

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
h : S.LeftHomologyData
⊢ h.leftHomologyIso.hom ≫ h.homologyIso.inv = S.leftHomologyIso.hom

Tactic:
by
  dsimp only [homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

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
h : S.RightHomologyData
⊢ h.rightHomologyIso.hom ≫ h.homologyIso.inv = S.rightHomologyIso.hom

Tactic:
by
  dsimp only [homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

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
φ : 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 : Cofork.π (CokernelCofork.ofπ S₂.homologyπ ⋯) ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ IsIso (homologyMap φ)

Tactic:
dsimp at hz

Goal state after:
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π
⊢ IsIso (homologyMap φ)
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
φ : 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 ≫ Fork.ι (KernelFork.ofι S₁.homologyι ⋯) = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ IsIso (homologyMap φ)

Tactic:
dsimp at hz

Goal state after:
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 φ)
⊢ IsIso (homologyMap φ)
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
⊢ IsColimit (CokernelCofork.ofπ (F.map h.π) wπ)

Tactic:
let e : parallelPair f' 0 ≅ parallelPair (F.map h.f') 0 :=
      parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa using hf') (by simp)

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₁ 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)) ⋯ ⋯
⊢ IsColimit (CokernelCofork.ofπ (F.map h.π) wπ)
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
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
let h₂' := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
  have : IsIso (rightHomologyMap' φ h₁ h₂') := by
    rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]
    dsimp
    infer_instance
  have eq := rightHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' h₂
  rw [comp_id] at eq
  rw [eq]
  infer_instance

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
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
⊢ (S.map F).RightHomologyData

Tactic:
have hι : IsLimit (KernelFork.ofι (F.map h.ι) wι) := by
    let e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
      parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa using hg') (by simp)
    refine IsLimit.postcomposeHomEquiv e _
      (IsLimit.ofIsoLimit (KernelFork.mapIsLimit _ h.hι' F) ?_)
    exact Fork.ext (Iso.refl _) (by simp [e])

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₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
hι : IsLimit (KernelFork.ofι (F.map h.ι) wι)
⊢ (S.map F).RightHomologyData
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
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ
wπ : f' ≫ cokernel.π (kernel.ι γ) = 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
Z'✝ : C
x : kernel S.g ⟶ Z'✝
hx : f' ≫ x = 0
⊢ kernel.ι γ ≫ x = 0

Tactic:
simpa only [← cancel_epi e.hom, ← cancel_epi (Abelian.factorThruImage S.f),
        comp_zero, fac, assoc] using hx

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

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

Tactic:
simp only [sub_eq_add_neg, opcyclesMap'_add, opcyclesMap'_neg]

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
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
wι : kernel.ι (cokernel.π γ) ≫ g' = 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
⊢ S.RightHomologyData

Tactic:
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_ι]))

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
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
wι : kernel.ι (cokernel.π γ) ≫ g' = 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
hι : IsLimit (KernelFork.ofι (kernel.ι (cokernel.π γ)) wι)
⊢ S.RightHomologyData
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.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ π = 0

Tactic:
by
    dsimp
    rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

Tactic:
rightHomologyMap'_add,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ₂ h₁ h₂ + rightHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    rightHomologyMap' φ₂ h₁ 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
⊢ (S.map F).Exact

Tactic:
by
  have : S.HasHomology := h.hasHomology
  rw [S.rightHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h
  rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_zero]

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✝ : S.HasHomology
h : S.RightHomologyData
hS : S.Exact
⊢ Mono h.g'

Tactic:
exact hS.mono_g' h

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
s s' : S.Splitting
h : s.r = s'.r
⊢ s = s'

Tactic:
by
  have := s.epi_g
  have eq := s.id
  rw [← s'.id, h, add_right_inj, cancel_epi S.g] at eq
  cases s
  congr

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso (Arrow.mk f).hom).hom ≫ image.map sq = imageSubobjectMap sq ≫ (imageSubobjectIso g).hom

Tactic:
simp [imageSubobjectMap]

Goal state after: