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.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ Nonempty (IsLimit c)

Tactic:
refine ⟨isLimitWhiskerEquiv F _ (isLimitOfReflects H ?_)⟩
    let hc' := (isLimitWhiskerEquiv F _).symm hc
    exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂

Tactic:
big_k.w

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
⊢ b ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ g₃ ≫
      pushout.inr g₁ g₂ ≫
        pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
          (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯ =
    g₄ ≫ pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
pushout.inr_desc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ g₃ ≫ pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    g₄ ≫ pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
this : g = pushout.inr (f ≫ g) f ≫ (asIso (pushout.inl (f ≫ g) f)).inv
⊢ P g

Tactic:
rw [this, cancel_right_of_respectsIso (P := P)]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
this : g = pushout.inr (f ≫ g) f ≫ (asIso (pushout.inl (f ≫ g) f)).inv
⊢ P (pushout.inr (f ≫ g) f)
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
⊢ ∀ (f : Fin (n + 1) → C), PreservesColimit (Discrete.functor f) F

Tactic:
have := preserves_fin_of_preserves_binary_and_initial n
    intro f
    apply
      preservesColimit_of_preserves_colimit_cocone
        (extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)) _
    apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
    let :=
      extendCofanIsColimit (fun i => F.obj (f i))
        (isColimitOfHasCoproductOfPreservesColimit F _)
        (isColimitOfHasBinaryCoproductOfPreservesColimit F _ _)
    refine IsColimit.ofIsoColimit this ?_
    apply Cocone.ext _ _
    · apply Iso.refl _
    rintro ⟨j⟩
    refine Fin.inductionOn j ?_ ?_
    · apply Category.comp_id
    · rintro i _
      dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι_app]
      rw [comp_id, ← F.map_comp]
      rfl

Goal state after:
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
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (fst A B) = fst (F.obj A) (F.obj B)

Tactic:
by simp [IsIso.inv_comp_eq]

Goal state after:
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
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (snd A B) = snd (F.obj A) (F.obj B)

Tactic:
by simp [IsIso.inv_comp_eq]

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

Goal state before:
pp: case h_fst
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
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ (μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv) ≫ fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y) =
    ((μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv) ≫ fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)

Tactic:
simp [← Functor.comp_obj, ← Functor.map_comp]

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

Goal state before:
pp: case h_snd
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
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ (μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv) ≫ snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y) =
    ((μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv) ≫ snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)

Tactic:
simp [← Functor.comp_obj, ← Functor.map_comp]

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:
by
  unfold raise'; cases l with grind [isChain_cons_raise']

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 ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ ¬l i = 0

Tactic:
← lc_def,

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 ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) (lc e l) ≠ 0
⊢ ¬l i = 0
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
convert! lift_rank_lt_rank_dual' h

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ RankCondition Rᵐᵒᵖ ↔ RankCondition R

Tactic:
by
  simp_rw [rankCondition_iff_matrix, ← opEquiv.mapMatrix.forall_congr_right,
    ← opEquiv.mapMatrix.symm.injective.eq_iff]
  congr! 2 with n m
  refine forall_comm.trans <| .trans (forall_congr' ?_) (transposeAddEquiv ..).forall_congr_right
  refine fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right
  rw [← (transposeAddEquiv ..).injective.eq_iff]
  congrm (?_ = ?_ → _)
  · ext; simp [map, mul_apply]
  · simp

Goal state after:
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
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ ¬finrank R M - finrank R ↥N = 0

Tactic:
tsub_eq_zero_iff_le,

Goal state after:
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
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ ¬finrank R M ≤ finrank R ↥N
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
        (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
          ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V)))
      ((Basis.ofVectorSpace K V).dualBasis j) =
    ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
        (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))))
      ((Basis.ofVectorSpace K V).dualBasis j)

Tactic:
apply LinearMap.ext_ring

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
            ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V)))
        ((Basis.ofVectorSpace K V).dualBasis j))
      1 =
    (((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))))
        ((Basis.ofVectorSpace K V).dualBasis j))
      1
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
⊢ (TensorProduct.mk K K V).compr₂ₛₗ
      (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)) =
    (TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))

Tactic:
apply LinearMap.ext_ring

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
⊢ ((TensorProduct.mk K K V).compr₂ₛₗ
        (LinearMap.lTensor V (contractLeft K V) ∘ₗ
          ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)))
      1 =
    ((TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 1
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
⊢ ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 =
    (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q) p)

Tactic:
by
  ext <;>
    simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

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

Goal state before:
pp: case refine_3.left
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
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.left } =
    (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.left }

pp: case refine_3.right
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
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.right } =
    (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.right }

Tactic:
· simp only [Category.assoc, ← G.map_comp, prod.lift_fst, BinaryFan.π_app_left,
              BinaryFan.mk_fst]

Goal state after:
case refine_3.right
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
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.right } =
    (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.right }
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr.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
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : 0 < (B y) y
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
rw [mul_comm (B x y), mul_comm (B x x)]
      exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux y x) hy

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

Goal state before:
pp: 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'
W : Submodule R M
⊢ W ≤ W.dualAnnihilator.subtype.flip.ker

Tactic:
by
    intro w hw
    ext ⟨φ, hφ⟩
    exact (mem_dualAnnihilator φ).mp hφ w hw

Goal state after:
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
⊢ (f ≫ biprod.inl + -g ≫ biprod.inr) ≫ s.π = 0

Tactic:
← neg_comp,

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
⊢ (f ≫ biprod.inl + (-g) ≫ biprod.inr) ≫ s.π = 0
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
r : x * b ∈ (Hom.hom f).range
⊢ b = x⁻¹ * (x * b)

Tactic:
← mul_assoc,

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
r : x * b ∈ (Hom.hom f).range
⊢ b = x⁻¹ * x * b
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
⊢ fromCoset ⟨y • ↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
fromCoset_eq_of_mem_range _ m

Goal state after:
case pos
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩
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
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this : d ≫ (-g) = 0
⊢ e = 0

Tactic:
have : d = 0 := (cancel_mono (-g)).1 (by simpa)

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
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ e = 0
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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ (eK.hom ≫ h.i) ≫ S.g = 0

Tactic:
rw [assoc, h.wi, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ (eH.hom ≫ h.ι ≫ eQ.inv) ≫ (IsCokernel.cokernelIso S.f (h.p ≫ eQ.inv) h.hp eQ.symm ⋯).desc (CokernelCofork.ofπ S.g ⋯) =
    0

Tactic:
simp [IsCokernel.cokernelIso]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ (parallelPair (h.hp.desc (CokernelCofork.ofπ S.g ⋯)) 0).map WalkingParallelPairHom.left ≫ (Iso.refl S.X₃).hom =
    eQ.symm.hom ≫
      (parallelPair ((IsCokernel.cokernelIso S.f (h.p ≫ eQ.inv) h.hp eQ.symm ⋯).desc (CokernelCofork.ofπ S.g ⋯)) 0).map
        WalkingParallelPairHom.left

Tactic:
simp [IsCokernel.cokernelIso]

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ ((Cone.postcompose (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯).hom).obj (KernelFork.ofι h.ι ⋯)).π.app
      WalkingParallelPair.zero =
    eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app WalkingParallelPair.zero

Tactic:
simp [IsCokernel.cokernelIso]

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

Goal state before:
pp: case one
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ ((Cone.postcompose (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯).hom).obj (KernelFork.ofι h.ι ⋯)).π.app
      WalkingParallelPair.one =
    eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app WalkingParallelPair.one

Tactic:
simp [IsCokernel.cokernelIso]

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
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
⊢ f' ≫ γ = 0

Tactic:
simp [γ, f']

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

Goal state before:
pp: case refine_1
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 ι
⊢ parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0 ≅
    parallelPair S.toCycles 0

Tactic:
exact parallelPair.ext (Iso.refl _) (S.isoCyclesOfIsLimit hkf)

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

Goal state before:
pp: case refine_2
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 ι
⊢ (Cocone.precompose
          (parallelPair.ext
              (Iso.refl
                ((parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                  WalkingParallelPair.zero))
              (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
      (CokernelCofork.ofπ π ⋯) ≅
    CokernelCofork.ofπ S.homologyπ ⋯

Tactic:
· exact Cofork.ext (isoHomology S hkf hcc fac) (by simp [Cofork.π])

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝¹ : L.PreservesMonomorphisms
adj : L ⊣ R
J : D
inst✝ : Injective J
A x✝ : C
g : A ⟶ R.obj J
f : A ⟶ x✝
im : Mono f
⊢ (adj.homEquiv A J).symm (f ≫ (adj.homEquiv x✝ J) (factorThru ((adj.homEquiv A J).symm g) (L.map f))) =
    (adj.homEquiv A J).symm g

Tactic:
simp [Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]

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
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ Epi S.toCycles ↔ Epi (kernel.lift S.g S.f ⋯)

Tactic:
apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff

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
⊢ Arrow.mk S.toCycles ≅ Arrow.mk (kernel.lift S.g S.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✝ : Preadditive D
S : ShortComplex C
h : S.Splitting
⊢ (h.s.op ≫ S.op.f + S.op.g ≫ h.r.op).unop = (𝟙 S.op.X₂).unop

Tactic:
simp only [op_X₂, Opposite.unop_op, op_X₁, op_f, op_X₃, op_g, unop_add, unop_comp,
      Quiver.Hom.unop_op, unop_id, ← h.id]

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✝¹ : Preadditive C
inst✝ : Preadditive D
S : ShortComplex C
h : S.Splitting
⊢ S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g

Tactic:
intro ⟨hS⟩
    exact ⟨S.exact_of_g_is_cokernel hS, epi_of_isColimit_cofork hS⟩

Goal state after: