mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ W.quotDualCoannihilatorToDual.SeparatingLeft ∧ W.quotDualCoannihilatorToDual.SeparatingRight

Tactic:
separatingLeft_iff_ker_eq_bot,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ W.quotDualCoannihilatorToDual.ker = ⊥ ∧ W.quotDualCoannihilatorToDual.SeparatingRight
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = s.ι
x : ↑s.pt
⊢ ↑((Hom.hom m) x) =
    ↑((Hom.hom (↟(LinearMap.codRestrict (Hom.hom f).ker (Hom.hom (Fork.ι (kernelCone f)) ∘ₗ Hom.hom m) ⋯))) x)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = s.ι
x : ↑s.pt
⊢ ↑((Hom.hom m) x) =
    ↑((Hom.hom (↟(LinearMap.codRestrict (Hom.hom f).ker (Hom.hom (Fork.ι (kernelCone f)) ∘ₗ Hom.hom m) ⋯))) x)
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: 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✝ : ↑M
⊢ (Hom.hom (f ≫ g)) x✝ = (Hom.hom 0) x✝

Tactic:
;

Goal state after:
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✝ : ↑M
⊢ (Hom.hom (f ≫ g)) x✝ = (Hom.hom 0) x✝
Module: Mathlib.Algebra.Category.FGModuleCat.Limits

Goal state before:
pp: J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type u
inst✝² : Ring k
J : Type
inst✝¹ : Finite J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), Module.Finite k ↑(Z j)
⊢ Module.Finite k
    ↑{ carrier := (j : J) → ↑(Z j), isAddCommGroup := Pi.addCommGroup, isModule := Pi.module J (fun j ↦ ↑(Z j)) k }

Tactic:
;

Goal state after:
J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type u
inst✝² : Ring k
J : Type
inst✝¹ : Finite J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), Module.Finite k ↑(Z j)
⊢ Module.Finite k
    ↑{ carrier := (j : J) → ↑(Z j), isAddCommGroup := Pi.addCommGroup, isModule := Pi.module J (fun j ↦ ↑(Z j)) k }
Module: Mathlib.Algebra.Category.FGModuleCat.Limits

Goal state before:
pp: J : Type
inst✝³ : SmallCategory J
inst✝² : FinCategory J
k : Type u
inst✝¹ : Ring k
inst✝ : IsNoetherianRing k
F : J ⥤ FGModuleCat k
⊢ Module.Finite k ↑(limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))

Tactic:
;

Goal state after:
J : Type
inst✝³ : SmallCategory J
inst✝² : FinCategory J
k : Type u
inst✝¹ : Ring k
inst✝ : IsNoetherianRing k
F : J ⥤ FGModuleCat k
⊢ Module.Finite k ↑(limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: 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)
x✝ : ↑M
⊢ (Hom.hom (f ≫ g)) x✝ = (Hom.hom 0) x✝

Tactic:
;

Goal state after:
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)
x✝ : ↑M
⊢ (Hom.hom (f ≫ g)) x✝ = (Hom.hom 0) x✝
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
j : J
⊢ (buildLimit (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯)).π.app j =
    (Iso.refl (buildLimit (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯)).pt).hom ≫
      (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t)))).π.app j

Tactic:
;

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
j : J
⊢ (buildLimit (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯)).π.app j =
    (Iso.refl (buildLimit (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯)).pt).hom ≫
      (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t)))).π.app j
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
j : J
⊢ G.map (equalizer.ι s t) ≫ G.map (Pi.π K.obj j) =
    𝟙 (G.obj (equalizer s t)) ≫ G.map (equalizer.ι s t ≫ limit.π (Discrete.functor K.obj) { as := j })

Tactic:
;

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
j : J
⊢ G.map (equalizer.ι s t) ≫ G.map (Pi.π K.obj j) =
    𝟙 (G.obj (equalizer s t)) ≫ G.map (equalizer.ι s t ≫ limit.π (Discrete.functor K.obj) { as := j })
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₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Surjective (⇑B.flip.dualMap ∘ ⇑(evalEquiv K V₁).toEquiv) ↔ Surjective ⇑B

Tactic:
;

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₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Surjective (⇑B.flip.dualMap ∘ ⇑(evalEquiv K V₁).toEquiv) ↔ Surjective ⇑B
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₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Injective ⇑B.dualMap

Tactic:
;

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₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Injective ⇑B.dualMap
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : Q ⟶ P := ⋯
t : Q ⟶ P := ⋯
I : C := ⋯
i : P ⟶ I := ⋯
⊢ IsColimit (Cofork.ofπ (G.map i) ⋯)

Tactic:
apply isColimitCoforkMapOfIsColimit

Goal state after:
case l
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : Q ⟶ P := ⋯
t : Q ⟶ P := ⋯
I : C := ⋯
i : P ⟶ I := ⋯
⊢ IsColimit (Cofork.ofπ i ?w)

case w
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : Q ⟶ P := ⋯
t : Q ⟶ P := ⋯
I : C := ⋯
i : P ⟶ I := ⋯
⊢ s ≫ i = t ≫ i
Module: Mathlib.CategoryTheory.Abelian.Images

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ (kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯) ≫ equalizer.ι (cokernel.π f) 0 = 0 ≫ equalizer.ι (cokernel.π f) 0

Tactic:
;

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ (kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯) ≫ equalizer.ι (cokernel.π f) 0 = 0 ≫ equalizer.ι (cokernel.π f) 0
Module: Mathlib.CategoryTheory.Abelian.Images

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f = coequalizer.π (kernel.ι f) 0 ≫ 0

Tactic:
;

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f = coequalizer.π (kernel.ι f) 0 ≫ 0
Module: Mathlib.Algebra.Category.ModuleCat.Abelian

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Mono f
x✝ : ↑(of R ↑M)
⊢ (Hom.hom
        ((((Hom.hom f).ker.quotEquivOfEqBot ⋯).symm ≪≫ₗ
                ((Hom.hom f).quotKerEquivRange ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom (↟(Hom.hom f).range.mkQ)).ker ⋯)).toModuleIso.hom ≫
          Fork.ι (kernelCone (↟(Hom.hom f).range.mkQ))))
      x✝ =
    (Hom.hom f) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Mono f
x✝ : ↑(of R ↑M)
⊢ (Hom.hom
        ((((Hom.hom f).ker.quotEquivOfEqBot ⋯).symm ≪≫ₗ
                ((Hom.hom f).quotKerEquivRange ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom (↟(Hom.hom f).range.mkQ)).ker ⋯)).toModuleIso.hom ≫
          Fork.ι (kernelCone (↟(Hom.hom f).range.mkQ))))
      x✝ =
    (Hom.hom f) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Abelian

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Epi f
x✝ : ↑M
⊢ (Hom.hom
        (Cofork.π (cokernelCocone (↟(Hom.hom f).ker.subtype)) ≫
          ((Hom.hom (↟(Hom.hom f).ker.subtype)).range.quotEquivOfEq (Hom.hom f).ker ⋯ ≪≫ₗ
                  (Hom.hom f).quotKerEquivRange ≪≫ₗ
                LinearEquiv.ofTop (Hom.hom f).range ⋯).toModuleIso.hom))
      x✝ =
    (Hom.hom f) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Epi f
x✝ : ↑M
⊢ (Hom.hom
        (Cofork.π (cokernelCocone (↟(Hom.hom f).ker.subtype)) ≫
          ((Hom.hom (↟(Hom.hom f).ker.subtype)).range.quotEquivOfEq (Hom.hom f).ker ⋯ ≪≫ₗ
                  (Hom.hom f).quotKerEquivRange ≪≫ₗ
                LinearEquiv.ofTop (Hom.hom f).range ⋯).toModuleIso.hom))
      x✝ =
    (Hom.hom f) x✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasKernel (cokernel.π f)
inst✝³ : PreservesColimit (parallelPair f 0) F
inst✝² : PreservesLimit (parallelPair (cokernel.π f) 0) F
inst✝¹ : HasCokernel (F.map f)
inst✝ : HasKernel (cokernel.π (F.map f))
⊢ (F.map (Abelian.factorThruImage f) ≫ (iso F f).hom) ≫ equalizer.ι (cokernel.π (F.map f)) 0 =
    Abelian.factorThruImage (F.map f) ≫ equalizer.ι (cokernel.π (F.map f)) 0

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasKernel (cokernel.π f)
inst✝³ : PreservesColimit (parallelPair f 0) F
inst✝² : PreservesLimit (parallelPair (cokernel.π f) 0) F
inst✝¹ : HasCokernel (F.map f)
inst✝ : HasKernel (cokernel.π (F.map f))
⊢ (F.map (Abelian.factorThruImage f) ≫ (iso F f).hom) ≫ equalizer.ι (cokernel.π (F.map f)) 0 =
    Abelian.factorThruImage (F.map f) ≫ equalizer.ι (cokernel.π (F.map f)) 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasCokernel (kernel.ι f)
inst✝³ : PreservesLimit (parallelPair f 0) F
inst✝² : PreservesColimit (parallelPair (kernel.ι f) 0) F
inst✝¹ : HasKernel (F.map f)
inst✝ : HasCokernel (kernel.ι (F.map f))
⊢ coequalizer.π (kernel.ι (F.map f)) 0 ≫ (iso F f).inv ≫ F.map (Abelian.factorThruCoimage f) =
    coequalizer.π (kernel.ι (F.map f)) 0 ≫ Abelian.factorThruCoimage (F.map f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasCokernel (kernel.ι f)
inst✝³ : PreservesLimit (parallelPair f 0) F
inst✝² : PreservesColimit (parallelPair (kernel.ι f) 0) F
inst✝¹ : HasKernel (F.map f)
inst✝ : HasCokernel (kernel.ι (F.map f))
⊢ coequalizer.π (kernel.ι (F.map f)) 0 ≫ (iso F f).inv ≫ F.map (Abelian.factorThruCoimage f) =
    coequalizer.π (kernel.ι (F.map f)) 0 ≫ Abelian.factorThruCoimage (F.map f)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| prod.lift a 0

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ

Tactic:
;

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| prod.lift a 0

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case a.f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a

pp: case a.g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ

Tactic:
;

Goal state after:
case a.f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a

case a.g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0 - a

Tactic:
;

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0 - a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
| a + b

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
| c

Tactic:
;

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
| a + b

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
| c
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)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
W : C
h : coequalizer u v ⟶ W
⊢ (w ≫ coequalizer.π u v) ≫ h = 0 ≫ h

Tactic:
eq_whisker hw

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
W : C
h : coequalizer u v ⟶ W
⊢ 0 ≫ h = 0 ≫ h
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
f g : Arrow C
u : f ⟶ g
⊢ (kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom = 0

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f✝ : X ⟶ Y
Z : C
g✝ : Y ⟶ Z
f g : Arrow C
u : f ⟶ g
⊢ (kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom = 0
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 : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u
⊢ e = 0

Tactic:
;

Goal state after:
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 : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u
⊢ e = 0
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 : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u
⊢ e = 0

Tactic:
;

Goal state after:
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 : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u
⊢ e = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ ≠ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
intro r

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ β⁻¹ • β • x = x

Tactic:
← mul_smul,

Goal state after:
A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (β⁻¹ * β) • x = x
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ β • β⁻¹ • x = x

Tactic:
← mul_smul,

Goal state after:
A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (β * β⁻¹) • x = x
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↑B
hz : (fun x ↦ x • ↑(Hom.hom f).range) z = ↑y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
;

Goal state after:
A B : GrpCat
f : A ⟶ B
x : ↑B
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↑B
hz : (fun x ↦ x • ↑(Hom.hom f).range) z = ↑y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)