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

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
⊢ FiniteDimensional K V

Tactic:
rw [FiniteDimensional, ← rank_lt_aleph0_iff]
  by_contra! contra
  suffices lift (Module.rank K V) < Module.rank K (Dual K (Dual K V)) by
    have heq := lift_rank_eq_of_equiv_equiv (R := K) (R' := K) (M := V) (M' := Dual K (Dual K V))
      (ZeroHom.id K) (evalEquiv K V) bijective_id (fun r v ↦ (evalEquiv K V).map_smul _ _)
    rw [← lift_umax, heq, lift_id'] at this
    exact lt_irrefl _ this
  have h₁ : lift (Module.rank K V) < Module.rank K (Dual K V) := lift_rank_lt_rank_dual contra
  have h₂ : Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V)) := by
    convert! lift_rank_lt_rank_dual <| le_trans (by simpa) h₁.le
    rw [lift_id']
  exact lt_trans h₁ h₂

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f ↦ F.obj f.fst.2
s✝ t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s✝ ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }
i : Fork s✝ t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
s : Cone F
j : J
⊢ hi.lift (Fork.ofι (t₁.lift (Fan.mk s.1 fun j ↦ s.π.app j)) ⋯) ≫ (buildLimit s✝ t hs ht i).π.app j = s.π.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : HasLimit (Discrete.functor F.obj)
inst✝¹ : HasLimit (Discrete.functor fun f ↦ F.obj f.fst.2)
inst✝ : HasEqualizers C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    (Pi.lift fun f ↦ limit.π (Discrete.functor F.obj) { as := f.fst.1 } ≫ F.map f.snd) ≫
        (limit.cone (Discrete.functor fun f ↦ F.obj f.fst.2)).π.app { as := f } =
      (limit.cone (Discrete.functor F.obj)).π.app { as := f.fst.1 } ≫ F.map f.snd

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : HasLimit (Discrete.functor F.obj)
inst✝¹ : HasLimit (Discrete.functor fun f ↦ F.obj f.fst.2)
inst✝ : HasEqualizers C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    (Pi.lift fun f ↦ limit.π (Discrete.functor F.obj) { as := f.fst.2 }) ≫
        (limit.cone (Discrete.functor fun f ↦ F.obj f.fst.2)).π.app { as := f } =
      (limit.cone (Discrete.functor F.obj)).π.app { as := f.fst.2 }

Tactic:
simp

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 : Subspace K V
x✝ : V
⊢ (∀ φ ∈ dualAnnihilator W, φ x✝ = 0) ↔ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator

Tactic:
simp

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 : Subspace K V
φ : Dual K ↥W
x : ↥W
⊢ ((dualRestrict W ∘ₗ W.dualLift) φ) x = (1 φ) x

Tactic:
simp

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
inst✝ : FiniteDimensional K V
W : Subspace K V
this : comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
← Module.mapEvalEquiv_symm_apply

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (mapEvalEquiv K V).symm (dualAnnihilator W).dualAnnihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W
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 : M
⊢ w ∈ W → w ∈ W.dualAnnihilator.subtype.flip.ker

Tactic:
hw

Goal state after:
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 : M
hw : w ∈ W
⊢ w ∈ W.dualAnnihilator.subtype.flip.ker
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 M
inst✝ : Projective R M
h : W.dualAnnihilator = ⊤
v : M
hv : v ∈ W
f : Dual R M
⊢ f v = 0

Tactic:
refine (mem_dualAnnihilator f).mp ?_ v hv

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
W : Submodule R M
inst✝ : Projective R M
h : W.dualAnnihilator = ⊤
v : M
hv : v ∈ W
f : Dual R M
⊢ f ∈ W.dualAnnihilator
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'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : f.rangeRestrict.dualMap.range = f.rangeRestrict.ker.dualAnnihilator
⊢ f.dualMap.range = (f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range

Tactic:
simp

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

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

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

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
⊢ f ≫ (BinaryCofan.mk (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)).ι.app { as := WalkingPair.left } =
    g ≫ ι₂ ≫ coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)

Tactic:
colimit.ι_desc

Goal state after:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
⊢ f ≫ (BinaryCofan.mk (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)).ι.app { as := WalkingPair.left } =
    g ≫ (BinaryCofan.mk (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)).ι.app { as := WalkingPair.right }
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
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s✝ t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s✝ = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s✝ t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
s : Cocone F
j : J
⊢ (buildColimit s✝ t hs ht i).ι.app j ≫ hi.desc (Cofork.ofπ (t₂.desc (Cofan.mk s.1 fun j ↦ s.ι.app j)) ⋯) = s.ι.app j

Tactic:
simp

Goal state after:
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
F : J ⥤ C
inst✝² : HasColimit (Discrete.functor F.obj)
inst✝¹ : HasColimit (Discrete.functor fun f ↦ F.obj f.fst.1)
inst✝ : HasCoequalizers C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    ((colimit.cocone (Discrete.functor fun f ↦ F.obj f.fst.1)).ι.app { as := f } ≫
        Sigma.desc fun f ↦ F.map f.snd ≫ colimit.ι (Discrete.functor F.obj) { as := f.fst.2 }) =
      F.map f.snd ≫ (colimit.cocone (Discrete.functor F.obj)).ι.app { as := f.fst.2 }

Tactic:
simp

Goal state after:
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
F : J ⥤ C
inst✝² : HasColimit (Discrete.functor F.obj)
inst✝¹ : HasColimit (Discrete.functor fun f ↦ F.obj f.fst.1)
inst✝ : HasCoequalizers C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    ((colimit.cocone (Discrete.functor fun f ↦ F.obj f.fst.1)).ι.app { as := f } ≫
        Sigma.desc fun f ↦ colimit.ι (Discrete.functor F.obj) { as := f.fst.1 }) =
      (colimit.cocone (Discrete.functor F.obj)).ι.app { as := f.fst.1 }

Tactic:
simp

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

Tactic:
simp

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

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

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

Tactic:
simp

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

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

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

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

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:
linearIndependent_iff_ker,

Goal state after:
ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ span F (Set.range (flip f)) = ⊤ ↔ (Finsupp.linearCombination F f).ker = ⊥
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:
simp

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

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

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

Tactic:
simp

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

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

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

Tactic:
simp

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

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

Goal state after:
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)
⊢ f ≫ cokernel.π f = 0

Tactic:
simp

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

Goal state after:
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 ≫ f = 0

Tactic:
simp

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

Goal state after:
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✝¹ : HasKernels C
inst✝ : HasCokernels C
f g : Arrow C
η : f ⟶ g
⊢ f.hom ≫ Arrow.Hom.right η = Arrow.Hom.left η ≫ g.hom

Tactic:
simp

Goal state after:
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✝¹ : HasKernels C
inst✝ : HasCokernels C
f g : Arrow C
η : f ⟶ g
⊢ kernel.ι f.hom ≫ Arrow.Hom.left η = kernel.map f.hom g.hom (Arrow.Hom.left η) (Arrow.Hom.right η) ⋯ ≫ kernel.ι g.hom

Tactic:
simp

Goal state after:
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✝¹ : HasKernels C
inst✝ : HasCokernels C
f g : Arrow C
η : f ⟶ g
⊢ cokernel.π f.hom ≫ cokernel.map f.hom g.hom (Arrow.Hom.left η) (Arrow.Hom.right η) ⋯ =
    Arrow.Hom.right η ≫ cokernel.π g.hom

Tactic:
simp

Goal state after:
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 := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (j : J),
    (G.map (Sigma.ι K.obj j) ≫ G.map (coequalizer.π s t)) ≫ 𝟙 (G.obj I) =
      G.map (colimit.ι (Discrete.functor K.obj) { as := j } ≫ coequalizer.π s t)

Tactic:
simp

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 : C
f g : X ⟶ Y
huv : pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) = pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)
hvu :
  pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f = pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g
huu :
  pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f = pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g
s : Fork f g
⊢ pullback.lift s.ι s.ι ⋯ ≫ (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).ι = s.ι

Tactic:
simp

Goal state after: