mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.zero =
    c.π.app WalkingParallelPair.zero

pp: case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.zero =
    c.π.app WalkingParallelPair.zero

case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case e'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushoutInl F =
    coprod.inl ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) =
    coprod.inl ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

Tactic:
<;>

Goal state after:
case e'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushoutInl F =
    coprod.inl ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) =
    coprod.inl ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.left ≫ pushoutInl F =
    coprod.inr ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.right ≫
      pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) =
    coprod.inr ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

Tactic:
<;>

Goal state after:
case e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.left ≫ pushoutInl F =
    coprod.inr ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

case e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.right ≫
      pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) =
    coprod.inr ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ (coequalizerCocone F).ι.app WalkingParallelPair.zero ≫
      pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.zero

pp: case one
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ (coequalizerCocone F).ι.app WalkingParallelPair.one ≫
      pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ (coequalizerCocone F).ι.app WalkingParallelPair.zero ≫
      pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.zero

case one
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ (coequalizerCocone F).ι.app WalkingParallelPair.one ≫
      pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.one
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)

Tactic:
have := e.lift_rank_eq

Goal state after:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this✝ : ℵ₀ ≤ Module.rank K V
this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.SeparatingLeft

Tactic:
intro m hB

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
m : M
hB : ∀ (y : M), (B m) y = 0
⊢ m = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.zero ≫
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
        pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.zero

pp: case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.one ≫
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
        pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.zero ≫
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
        pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.zero

case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.one ≫
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
        pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.one
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case hl
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
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  (dualProdDualEquivDual R M N).dualMap ≪≫ₗ (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
m : M
f : Dual R (M × N)
⊢ ((Dual.eval R (M × N) ∘ₗ inl R M N) m) f = (((↑e.symm ∘ₗ (Dual.eval R M).prodMap (Dual.eval R N)) ∘ₗ inl R M N) m) f

pp: case hr
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
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  (dualProdDualEquivDual R M N).dualMap ≪≫ₗ (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
m : N
f : Dual R (M × N)
⊢ ((Dual.eval R (M × N) ∘ₗ inr R M N) m) f = (((↑e.symm ∘ₗ (Dual.eval R M).prodMap (Dual.eval R N)) ∘ₗ inr R M N) m) f

Tactic:
<;>

Goal state after:
case hl
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
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  (dualProdDualEquivDual R M N).dualMap ≪≫ₗ (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
m : M
f : Dual R (M × N)
⊢ ((Dual.eval R (M × N) ∘ₗ inl R M N) m) f = (((↑e.symm ∘ₗ (Dual.eval R M).prodMap (Dual.eval R N)) ∘ₗ inl R M N) m) f

case hr
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
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  (dualProdDualEquivDual R M N).dualMap ≪≫ₗ (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
m : N
f : Dual R (M × N)
⊢ ((Dual.eval R (M × N) ∘ₗ inr R M N) m) f = (((↑e.symm ∘ₗ (Dual.eval R M).prodMap (Dual.eval R N)) ∘ₗ inr R M N) m) f
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (𝟙 Z) = 𝟙 (F.obj Z)

Tactic:
F.map_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ 𝟙 (F.obj Z) = 𝟙 (F.obj Z)
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (𝟙 Y) = 𝟙 (F.obj Y)

Tactic:
F.map_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ 𝟙 (F.obj Y) = 𝟙 (F.obj Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map (𝟙 W) = 𝟙 (F.obj W)

Tactic:
F.map_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ 𝟙 (F.obj W) = 𝟙 (F.obj W)
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map (𝟙 X) = 𝟙 (F.obj X)

Tactic:
F.map_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inl
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
⊢ 0 ≤ (B 0) 0

pp: case inr
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y z : M
hz : z ≠ 0
⊢ 0 ≤ (B z) z

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
⊢ 0 ≤ (B 0) 0

case inr
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y z : M
hz : z ≠ 0
⊢ 0 ≤ (B z) z
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
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual R (M ⧸ W))

Tactic:
W.dualQuotEquivDualAnnihilator.toEquiv.subsingleton_congr,

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
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton ↥W.dualAnnihilator
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)
⊢ (kernelCone g).π.app WalkingParallelPair.zero =
    (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

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)
⊢ (kernelCone g).π.app WalkingParallelPair.one =
    (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

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)
⊢ (kernelCone g).π.app WalkingParallelPair.zero =
    (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

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)
⊢ (kernelCone g).π.app WalkingParallelPair.one =
    (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