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

Goal state before:
pp: case right.right.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b : J.R
⊢ (hom (𝟙 ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right b)))) ((hom (I.fst b)) (↑x (J.fst b))) =
    (hom (I.fst b)) (↑x (J.fst b))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
J : MulticospanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.fst a✝))).comp (Hom.fst a✝) = Hom.fst a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.snd a✝))).comp (Hom.snd a✝) = Hom.snd a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.fst a✝).comp (Hom.id (right a✝)) = Hom.fst a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.snd a✝).comp (Hom.id (right a✝)) = Hom.snd a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case left
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
a : J.L
⊢ ↑((fun x ↦
            ⟨fun j ↦
              match j with
              | WalkingMulticospan.left a => ↑x a
              | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
              ⋯⟩)
          ((fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩) x))
      (WalkingMulticospan.left a) =
    ↑x (WalkingMulticospan.left a)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case right
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
b : J.R
⊢ ↑((fun x ↦
            ⟨fun j ↦
              match j with
              | WalkingMulticospan.left a => ↑x a
              | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
              ⋯⟩)
          ((fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩) x))
      (WalkingMulticospan.right b) =
    (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst b))) (↑x (WalkingMulticospan.left (J.fst b)))

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom 0) x = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
i : J.L
⊢ ↑((fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩)
          ((fun x ↦
              ⟨fun j ↦
                match j with
                | WalkingMulticospan.left a => ↑x a
                | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
                ⋯⟩)
            x))
      i =
    ↑x i

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.left.id.id.id
J : MulticospanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.id (left a✝)) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.id (left a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.right.id.id.fst
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.fst a✝))).comp (Hom.id (left (J.fst a✝)))).comp (Hom.fst a✝) =
    (Hom.id (left (J.fst a✝))).comp ((Hom.id (left (J.fst a✝))).comp (Hom.fst a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.right.id.id.snd
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.snd a✝))).comp (Hom.id (left (J.snd a✝)))).comp (Hom.snd a✝) =
    (Hom.id (left (J.snd a✝))).comp ((Hom.id (left (J.snd a✝))).comp (Hom.snd a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.right.right.id.fst.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.fst a✝))).comp (Hom.fst a✝)).comp (Hom.id (right a✝)) =
    (Hom.id (left (J.fst a✝))).comp ((Hom.fst a✝).comp (Hom.id (right a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.right.right.id.snd.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.snd a✝))).comp (Hom.snd a✝)).comp (Hom.id (right a✝)) =
    (Hom.id (left (J.snd a✝))).comp ((Hom.snd a✝).comp (Hom.id (right a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.right.right.fst.id.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.fst a✝).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.fst a✝).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.right.right.snd.id.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.snd a✝).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.snd a✝).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.right.right.id.id.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (right a✝)).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.id (right a✝)).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case h
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (hom (head f)) y = (hom (colimit.ι (wideSpan B X f) none)) y

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case h
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (hom (ι f j)) y = (hom (colimit.ι (wideSpan B X f) (some j))) y

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ F.obj (WalkingMulticospan.left a✝) = G.obj (WalkingMulticospan.left a✝)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.R
⊢ F.obj (WalkingMulticospan.right a✝) = G.obj (WalkingMulticospan.right a✝)

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (∀ (x₂ : ↑(S.map (forget₂ C Ab)).X₂),
      (ConcreteCategory.hom (S.map (forget₂ C Ab)).g) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom (S.map (forget₂ C Ab)).f) x₁ = x₂) ↔
    ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)),
      (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x₁ = x₂

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.fst a✝) = Hom.fst a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.snd a✝) = Hom.snd a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
J : MultispanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.fst a✝).comp (Hom.id (right (J.fst a✝))) = Hom.fst a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.snd a✝).comp (Hom.id (right (J.snd a✝))) = Hom.snd a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.left.id.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.id (left a✝)) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.id (left a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.right.id.id.fst
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.fst a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.fst a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.right.id.id.snd
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.snd a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.snd a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.right.right.id.fst.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.fst a✝)).comp (Hom.id (right (J.fst a✝))) =
    (Hom.id (left a✝)).comp ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝))))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.right.right.id.snd.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.snd a✝)).comp (Hom.id (right (J.snd a✝))) =
    (Hom.id (left a✝)).comp ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝))))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.right.right.fst.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝)))).comp (Hom.id (right (J.fst a✝))) =
    (Hom.fst a✝).comp ((Hom.id (right (J.fst a✝))).comp (Hom.id (right (J.fst a✝))))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.right.right.snd.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝)))).comp (Hom.id (right (J.snd a✝))) =
    (Hom.snd a✝).comp ((Hom.id (right (J.snd a✝))).comp (Hom.id (right (J.snd a✝))))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.right.right.id.id.id
J : MultispanShape
a✝ : J.R
⊢ ((Hom.id (right a✝)).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.id (right a✝)).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case id
J : MultispanShape
a : WalkingMultispan J
⊢ Hom.id a = 𝟙 a

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
J : MultispanShape
a✝ : J.L
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (left a✝)) =
    left a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
J : MultispanShape
a✝ : J.R
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (right a✝)) =
    right a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inl
J : MultispanShape
val✝ : J.L
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inl val✝)) =
    Sum.inl val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inr
J : MultispanShape
val✝ : J.R
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inr val✝)) =
    Sum.inr val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case id
J : MultispanShape
left✝ : WalkingMultispan J
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }) =
    { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case fst
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }) =
    { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case snd
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }) =
    { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
⊢ (↑eL.symm ∘ₗ g ∘ₗ ↑eN) ∘ₗ (↑eN.symm ∘ₗ f) ∘ₗ ↑eM = 0

Tactic:
ext x
      simpa using LinearMap.congr_fun eq0 (eM x)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inl
J : MultispanShape
val✝ : WalkingMultispan J
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inl val✝)) =
    Sum.inl val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inr.inl
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inl val✝))) =
    Sum.inr (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inr.inr
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inr val✝))) =
    Sum.inr (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.L
⊢ (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝, 𝟙 (WalkingMulticospan.left a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.R
⊢ (match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝, 𝟙 (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, 𝟙 (WalkingMultispan.left a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.R
⊢ (match WalkingMultispan.right a✝, WalkingMultispan.right a✝, 𝟙 (WalkingMultispan.right a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: case left.left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ (((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map { down := { down := ⋯ } } ≫
      Discrete.casesOn { as := WalkingPair.left } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) =
    (Discrete.casesOn { as := WalkingPair.left } fun j ↦
        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) ≫
      (pair M N).map { down := { down := ⋯ } }

Tactic:
rfl

Goal state after: