mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ IsIso (kernelComparison f G)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
by

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : IsCompl W W'
⊢ IsCompl (dualAnnihilator W) (dualAnnihilator W')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ (PreservesKernel.iso G g).inv =
    (PreservesKernel.iso G f).inv ≫ G.map (kernel.map f g p q hpq)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map f ≫ G.map (Cofork.π c) = 0

Tactic:
by

Goal state after:
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.dualMap.range = finrank K ↥f.range

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ∀ (j : WalkingParallelPair),
    ((Cocone.precompose
                    (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
                (G.mapCocone c)).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose
                    (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
                (G.mapCocone c)).pt).hom =
      (c.map G).ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ IsColimit (G.mapCocone c) ≃ IsColimit (c.map G)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝¹ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝ : PreservesColimit (parallelPair f 0) G
l : IsColimit (CokernelCofork.ofπ h w)
⊢ G.map f ≫ G.map h = 0

Tactic:
by

Goal state after:
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₂
⊢ Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ G.map f ≫ G.map (cokernel.π f) = 0 ≫ G.map (cokernel.π f)

Tactic:
by

Goal state after:
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₂
⊢ Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
by

Goal state after:
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✝ : IsReflexive K V₂
⊢ B.ker.dualAnnihilator = B.flip.range

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ (iso G f).inv = cokernelComparison f G

Tactic:
by

Goal state after:
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 ↔ Surjective ⇑B

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ IsIso (cokernelComparison f G)

Tactic:
by

Goal state after:
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 ↔ Surjective ⇑B

Tactic:
by

Goal state after:
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₁
⊢ Bijective ⇑B.flip ↔ Bijective ⇑B

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : NormalMono.Z (F.map f) ⟶ W
⊢ F.map f ≫ NormalMono.g ≫ h = 0 ≫ h

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (f ≫ F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) = F.map 0

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) ≫
      (F.objObjPreimageIso (NormalMono.Z (F.map f))).hom =
    NormalMono.g

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ (Iso.refl (KernelFork.ofι (Fork.ι (KernelFork.ofι (F.map f) ⋯)) ⋯).pt).hom ≫
      Fork.ι ((Cone.postcomposeEquivalence (compNatIso F)).functor.obj (F.mapCone (KernelFork.ofι f ⋯))) =
    Fork.ι (KernelFork.ofι (Fork.ι (KernelFork.ofι (F.map f) ⋯)) ⋯)

Tactic:
by

Goal state after:
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
f : X ⟶ Y
I : NormalMono f
⊢ f ≫ g = f ≫ 0

Tactic:
by

Goal state after:
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
W : C
h' : S ⟶ W
⊢ f ≫ h ≫ h' = g ≫ k ≫ h'

Tactic:
by

Goal state after:
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ NormalMono.g = 0

Tactic:
by

Goal state after:
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (KernelFork.ofι g ⋯)

Tactic:
by

Goal state after:
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 : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ f' ≫ Arrow.Hom.right e.inv ≫ g = 0

Tactic:
by

Goal state after:
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 : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ IsLimit (KernelFork.ofι f' ⋯)

Tactic:
by

Goal state after:
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
inst✝ : IsNormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ IsRegularMono f

Tactic:
by

Goal state after:
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
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ F.map (F.preimage ((F.objObjPreimageIso (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f) = F.map 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ (PreservesCokernel.iso G f).hom ≫ cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ =
    G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G g).hom

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ (F.objObjPreimageIso (NormalEpi.W (F.map f))).symm.hom ≫
      F.map (F.preimage ((F.objObjPreimageIso (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g)) =
    NormalEpi.g

Tactic:
by

Goal state after:
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 (Dual K V)
inst✝ : FiniteDimensional K V
⊢ map (Dual.eval K V) (dualCoannihilator W) = dualAnnihilator W

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ Cofork.π (CokernelCofork.ofπ (Cofork.π (CokernelCofork.ofπ (F.map f) ⋯)) ⋯) ≫
      (Iso.refl (CokernelCofork.ofπ (Cofork.π (CokernelCofork.ofπ (F.map f) ⋯)) ⋯).pt).hom =
    Cofork.π ((Cocone.precomposeEquivalence (compNatIso F)).functor.obj (F.mapCocone (CokernelCofork.ofπ f ⋯)))

Tactic:
by

Goal state after:
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
f : X ⟶ Y
I : NormalEpi f
⊢ g ≫ f = 0 ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ (G.mapIso (asIso (Fork.ι c))).symm.hom ≫ Fork.ι (KernelFork.map c G) = Fork.ι (KernelFork.ofι (𝟙 (G.obj X)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)

Tactic:
by

Goal state after:
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
⊢ NormalEpi.g ≫ g ≫ h' = 0 ≫ h'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ Cofork.π (CokernelCofork.ofπ (𝟙 (G.obj Y)) ⋯) ≫ (G.mapIso (asIso (Cofork.π c))).hom =
    Cofork.π (CokernelCofork.map c G)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cocone (parallelPair 0 0)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)

Tactic:
by

Goal state after:
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (NormalEpi.g ≫ f) ≫ h = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
by

Goal state after:
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (CokernelCofork.ofπ h ⋯)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ span F (Set.range (flip f)) = ⊤ ↔ LinearIndependent F f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
⊢ ⊤ ≤ span K (Set.range fun x ↦ id ↑x)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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'
⊢ Cofork.π
        ((Cocone.precompose
              (parallelPair.ext (Iso.refl ((parallelPair g 0).obj WalkingParallelPair.zero)) (Arrow.leftFunc.mapIso e) ⋯
                  ⋯).inv).obj
          (CokernelCofork.ofπ f ⋯)) ≫
      (Arrow.rightFunc.mapIso e).hom =
    Cofork.π (CokernelCofork.ofπ f' ⋯)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ hli.extend ⋯
ri : ↑(hli.extend ⋯) := ⟨v i, hi⟩
⊢ b ri = v i

Tactic:
by

Goal state after:
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'
⊢ IsColimit (CokernelCofork.ofπ f' ⋯)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K v s
⊢ ∃ f, ∀ i ∈ s, f (v i) = 1

Tactic:
by

Goal state after:
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✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
⊢ kernel.ι (prod.lift f g) ≫ f = kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ prod.fst

Tactic:
by

Goal state after:
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✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
⊢ kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ prod.fst = 0 ≫ prod.fst

Tactic:
by

Goal state after:
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
m : NormalMono f.unop
⊢ ∀ {Z' : Cᵒᵖ} (g' : X ⟶ Z') (eq' : NormalMono.g.op ≫ g' = 0) (m_1 : Y ⟶ Z'),
    f ≫ m_1 = g' → m_1 = (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop ⋯)).op

Tactic:
by

Goal state after: