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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ η_ X' Y ▷ X ⊗≫ (i.inv ▷ (Y ⊗ X) ≫ X ◁ Y ◁ i.hom) ⊗≫ X ◁ ε_ X' Y =
    𝟙 (𝟙_ C ⊗ X) ⊗≫ (η_ X' Y ▷ X ≫ (X' ⊗ Y) ◁ i.hom) ⊗≫ (i.inv ▷ (Y ⊗ X') ≫ X ◁ ε_ X' Y) ⊗≫ 𝟙 (X ⊗ 𝟙_ C)

Tactic:
by
        rw [← whisker_exchange]; monoidal

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
⊢ B.IsRefl

Tactic:
intro x y h

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : (B x) y = 0
⊢ (B y) x = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left = pullbackFst F ≫ F.map WalkingParallelPairHom.right

Tactic:
conv_rhs => rw [pullbackFst_eq_pullback_snd]
        convert!
          (eq_whisker pullback.condition Limits.prod.snd :
            (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _) using
          1 <;> simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e
hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e
he : Function.Surjective ⇑↑e
⊢ B.IsPairSelfAdjoint F ⇑f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) ⇑(e.symm.conj f)

Tactic:
IsPairSelfAdjoint,

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e
hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e
he : Function.Surjective ⇑↑e
⊢ B.IsAdjointPair F ⇑f ⇑f ↔ (B.compl₁₂ ↑e ↑e).IsAdjointPair (F.compl₁₂ ↑e ↑e) ⇑(e.symm.conj f) ⇑(e.symm.conj f)
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
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h : Function.Surjective ⇑↑e
f : P
q : Dual R M
m : Q
x✝ : M
⊢ ((((TensorProduct.mk R (Dual R M) Q).compr₂ₛₗ
            (((TensorProduct.mk R P (Dual R M ⊗[R] Q)).compr₂ₛₗ (↑(lTensorHomEquivHomLTensor R M P Q) ∘ₗ ↑e)) f))
          q)
        m)
      x✝ =
    ((((TensorProduct.mk R (Dual R M) Q).compr₂ₛₗ
            (((TensorProduct.mk R P (Dual R M ⊗[R] Q)).compr₂ₛₗ (lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ ↑e)) f))
          q)
        m)
      x✝

Tactic:
simp [e, lTensorHomEquivHomLTensor]

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

Goal state before:
pp: case e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : f.rangeRestrict.dualMap.range = f.rangeRestrict.ker.dualAnnihilator
⊢ (f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range = f.rangeRestrict.dualMap.range

Tactic:
← dualMap_comp_dualMap,

Goal state after:
case e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : f.rangeRestrict.dualMap.range = f.rangeRestrict.ker.dualAnnihilator
⊢ (f.rangeRestrict.dualMap ∘ₗ f.range.subtype.dualMap).range = f.rangeRestrict.dualMap.range
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K ↥(f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range = finrank K ↥f.range

Tactic:
← dualMap_comp_dualMap,

Goal state after:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K ↥(f.rangeRestrict.dualMap ∘ₗ f.range.subtype.dualMap).range = finrank K ↥f.range
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K ↥(map (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Tactic:
rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]

Goal state after:
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
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 : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
⊢ u = v

Tactic:
obtain ⟨m, hm⟩ := coequalizer.desc' f huv

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 : C
f : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
⊢ u = v
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
Z : C
g : Y ⟶ Z
⊢ Limits.image.ι f ≫ cokernel.π f = 0

Tactic:
by simp [← cancel_epi (factorThruImage f)]

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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ e = biprod.inr ≫ biprod.desc 0 e

Tactic:
rw [biprod.inr_desc]

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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ (-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d

Tactic:
rw [biprod.inr_desc]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞)
      ((g x) ((Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞) (fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩))) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

Tactic:
@Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) ∞
      (fromCoset ⟨b • ↑f.hom.range, b, rfl⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)

Goal state after:
A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞) ((g x) (fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩)) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
a✝ : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Tactic:
exact quasiIso_of_comp_right φ φ'

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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ h₁.f' ≫ h₁.i ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i

Tactic:
LeftHomologyData.f'_i_assoc,

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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
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
inst✝ : S.HasLeftHomology
hg : S.g = 0
⊢ S.cycles ≅ S.X₂

Tactic:
by
  have := S.isIso_iCycles hg
  exact asIso S.iCycles

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₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.f' ≫ h₁.i ≫ h₂.p = 0 ≫ h₂.ι

Tactic:
LeftHomologyData.f'_i_assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ S.f ≫ h₂.p = 0 ≫ h₂.ι
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
⊢ (homologyMap φ).op = S₂.homologyOpIso.inv ≫ homologyMap (opMap φ) ≫ S₁.homologyOpIso.hom

Tactic:
dsimp only [homologyMap, homologyOpIso]
  rw [homologyMap'_op]
  dsimp only [Iso.symm, Iso.trans, Iso.op, Iso.refl, rightHomologyIso, leftHomologyIso,
    leftHomologyOpIso, leftHomologyMapIso', rightHomologyMapIso',
    LeftHomologyData.leftHomologyIso, homologyMap']
  simp only [assoc, rightHomologyMap'_op, op_comp, ← leftHomologyMap'_comp_assoc, id_comp,
    opMap_id, comp_id, HomologyData.op_left]

Goal state after:
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
eq₂ : ∀ (j : J), h₂.lift (π₂.mapCone s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₃ : ∀ (j : J), h₃.lift (π₃.mapCone s) ≫ (c.π.app j).τ₃ = (s.π.app j).τ₃
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = c.pt.g ≫ (c.π.app j).τ₃
eq₂₃' : ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ (s.π.app j).τ₃
⊢ (h₂.lift (π₂.mapCone s) ≫ c.pt.g) ≫ (c.π.app j).τ₃ = (s.pt.g ≫ h₃.lift (π₃.mapCone s)) ≫ (c.π.app j).τ₃

Tactic:
rw [assoc, assoc, ← eq₂₃, reassoc_of% eq₂, eq₃, eq₂₃']

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
⊢ S.RightHomologyData

Tactic:
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]

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
⊢ S.RightHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ F.map (leftHomologyMap φ) ≫ (S₂.mapLeftHomologyIso F).inv =
    (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)

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

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ (S₁.mapLeftHomologyIso F).hom ≫ F.map (leftHomologyMap φ) ≫ (S₂.mapLeftHomologyIso F).inv =
    (S₁.mapLeftHomologyIso F).hom ≫ (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: case h₂
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
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x✝, τ₂ := colimit.ι (F ⋙ π₂) x✝, τ₃ := colimit.ι (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    ({ τ₁ := colimit.ι (F ⋙ π₁) x✝¹, τ₂ := colimit.ι (F ⋙ π₂) x✝¹, τ₃ := colimit.ι (F ⋙ π₃) x✝¹, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        ((const J).obj
              { X₁ := colimit (F ⋙ π₁), X₂ := colimit (F ⋙ π₂), X₃ := colimit (F ⋙ π₃),
                f := colimMap (F.whiskerLeft π₁Toπ₂), g := colimMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f).τ₂

Tactic:
simp [← colimit.w (F ⋙ π₂) f]

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
⊢ H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i

Tactic:
LeftHomologyData.f'_i_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : 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 = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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

Tactic:
have := hS.hasHomology
  have := hS.mono_fromOpcycles
  have : S.pOpcycles = 0 := by rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
  apply Preadditive.epi_of_cancel_zero
  intro A x₂ hx₂
  rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]

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 : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)

Tactic:
rw [← F.map_comp, f_r, F.map_id]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
X₁ X₂ : Subobject X
h : (map f).obj X₁ = (map f).obj X₂
⊢ X₁ = X₂

Tactic:
by
  induction X₁ using Subobject.ind
  induction X₂ using Subobject.ind
  simp only [map_mk] at h
  exact mk_eq_mk_of_comm _ _ (isoOfMkEqMk _ _ h) (by simp [← cancel_mono f])

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ Mono (imageToKernel f g w)

Tactic:
dsimp only [imageToKernel]
  infer_instance

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

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
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)
S : ShortComplex C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
T : ShortComplex C := { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }
⊢ F.map (Abelian.factorThruImage S.f) ≫ F.map (kernel.ι (cokernel.π S.f)) = F.map S.f ≫ 𝟙 (F.obj S.X₂)

Tactic:
rw [← F.map_comp, Abelian.image.fac, Category.comp_id]

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

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

Tactic:
dsimp at hS

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ f.app i ≫ (L.lanUnit.app Y✝).app i ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).inv ≫ colimMap (L.lan.map f)

Tactic:
ι_colimitIsoOfIsLeftKanExtension_inv_assoc,

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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ f.app i ≫ (L.lanUnit.app Y✝).app i ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    (L.lanUnit.app X✝).app i ≫ colimit.ι (L.lan.obj X✝) (L.obj i) ≫ colimMap (L.lan.map f)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
⊢ AB5StarOfSize.{w, w', v, u} C

Tactic:
have : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
⊢ AB5StarOfSize.{w, w', v, u} C
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
⊢ StructuredArrow.hom (Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X)) ≫
      ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map
        (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y

Tactic:
ext Z f
        convert! (Y.hom.naturality_apply f.op _).symm
        simp

Goal state after: