mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.zero)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero))
      x

pp: case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.one)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one))
      x

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.zero)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero))
      x

case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.one)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one))
      x
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

pp: case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one
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₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
⊢ F.dualMap.range ≤ dualAnnihilator W ⊔ dualAnnihilator W'
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.left

pp: case refine_1.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.right

Tactic:
<;>

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.left

case refine_1.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.right
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left

pp: case refine_1.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right

Tactic:
<;>

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left

case refine_1.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ (g ≫ Arrow.Hom.left e.hom) ≫ f' = 0

Tactic:
have := Arrow.w e.hom
    dsimp at this
    rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]

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

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case zero
R : Type u_1
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
z : M ⊗[R] N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) z

pp: case tmul
R : Type u_1
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
z : M ⊗[R] N
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) z

pp: case add
R : Type u_1
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
z : M ⊗[R] N
x✝ y✝ : Dual R N ⊗[R] Dual R M
a✝¹ :
  ((dualDistrib R N M) x✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝)) z
a✝ :
  ((dualDistrib R N M) y✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝)) z
⊢ ((dualDistrib R N M) (x✝ + y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ + y✝))) z

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
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
z : M ⊗[R] N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) z

case tmul
R : Type u_1
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
z : M ⊗[R] N
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) z

case add
R : Type u_1
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
z : M ⊗[R] N
x✝ y✝ : Dual R N ⊗[R] Dual R M
a✝¹ :
  ((dualDistrib R N M) x✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝)) z
a✝ :
  ((dualDistrib R N M) y✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝)) z
⊢ ((dualDistrib R N M) (x✝ + y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ + y✝))) z
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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: case refine_1.h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
⊢ ((s.ι ≫ prod.fst) ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp)) ≫ prod.fst = s.ι ≫ prod.fst

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
⊢ ((s.ι ≫ prod.fst) ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp)) ≫ prod.snd = s.ι ≫ prod.snd

Tactic:
<;>

Goal state after:
case refine_1.h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
⊢ ((s.ι ≫ prod.fst) ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp)) ≫ prod.fst = s.ι ≫ prod.fst

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
⊢ ((s.ι ≫ prod.fst) ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp)) ≫ prod.snd = s.ι ≫ prod.snd
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case e'_3.h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ ((s.ι ≫ prod.fst) ≫ prod.lift (𝟙 A) 0) ≫ prod.fst = s.ι ≫ prod.fst

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ ((s.ι ≫ prod.fst) ≫ prod.lift (𝟙 A) 0) ≫ prod.snd = s.ι ≫ prod.snd

Tactic:
<;>

Goal state after:
case e'_3.h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ ((s.ι ≫ prod.fst) ≫ prod.lift (𝟙 A) 0) ≫ prod.fst = s.ι ≫ prod.fst

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ ((s.ι ≫ prod.fst) ≫ prod.lift (𝟙 A) 0) ≫ prod.snd = s.ι ≫ prod.snd
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ Fork.ι (pullbackToBiproductFork f g)) ≫ biprod.fst =
    s.ι ≫ biprod.fst

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ Fork.ι (pullbackToBiproductFork f g)) ≫ biprod.snd =
    s.ι ≫ biprod.snd

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ Fork.ι (pullbackToBiproductFork f g)) ≫ biprod.fst =
    s.ι ≫ biprod.fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ Fork.ι (pullbackToBiproductFork f g)) ≫ biprod.snd =
    s.ι ≫ biprod.snd
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.fst f g = pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullback.fst f g

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.snd f g = pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullback.snd f g

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.fst f g = pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullback.fst f g

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.snd f g = pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullback.snd f g
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₀
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.inl ≫ Cofork.π (biproductToPushoutCofork f g) ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ =
    biprod.inl ≫ s.π

pp: case h₁
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.inr ≫ Cofork.π (biproductToPushoutCofork f g) ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ =
    biprod.inr ≫ s.π

Tactic:
<;>

Goal state after:
case h₀
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.inl ≫ Cofork.π (biproductToPushoutCofork f g) ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ =
    biprod.inl ≫ s.π

case h₁
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.inr ≫ Cofork.π (biproductToPushoutCofork f g) ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ =
    biprod.inr ≫ s.π
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₀
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
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = s.π
⊢ pushout.inl f g ≫ m = pushout.inl f g ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

pp: case h₁
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
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = s.π
⊢ pushout.inr f g ≫ m = pushout.inr f g ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
<;>

Goal state after:
case h₀
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
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = s.π
⊢ pushout.inl f g ≫ m = pushout.inl f g ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

case h₁
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
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = s.π
⊢ pushout.inr f g ≫ m = pushout.inr f g ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono s.inr

Tactic:
have : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.right) :=
    Abelian.mono_pushout_of_mono_f f g

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.right)
⊢ Mono s.inr