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

Goal state before:
pp: J : MultispanShape
⊢ ∀ {W X Y Z : WalkingMultispan J} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by

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 v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this : PreservesFiniteLimits (forget₂ C Ab)
⊢ PreservesFiniteLimits (forget C)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ (right (J.fst i)).hom = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ (right (J.snd i)).hom = (left i).hom ≫ G.map (Hom.snd i)
⊢ ∀ {X Y : WalkingMultispan J} (f : X ⟶ Y),
    F.map f ≫
        (match Y with
          | WalkingMultispan.left i => left i
          | WalkingMultispan.right i => right i).hom =
      (match X with
          | WalkingMultispan.left i => left i
          | WalkingMultispan.right i => right i).hom ≫
        G.map f

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
a : WalkingMultispan J
⊢ ∀ (a_1 : a ⟶ a), a_1 = 𝟙 a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
a b : J.L
h : ¬a = b
⊢ ∀ (a : left a ⟶ left b), False

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
a b : J.L
⊢ Subsingleton (left a ⟶ left b)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
a b : J.R
h : ¬a = b
⊢ ∀ (a : right a ⟶ right b), False

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
a b : J.R
⊢ Subsingleton (right a ⟶ right b)

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
a : J.R
b : J.L
⊢ ∀ (a : right a ⟶ left b), False

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u // J.fst l = r' }
T₂ : Type := { u // J.snd l = r' }
x✝ : T₁
val✝ : Unit
h : J.fst l = r'
⊢ left l ⟶ right r'

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u // J.fst l = r' }
T₂ : Type := { u // J.snd l = r' }
x✝ : T₂
val✝ : Unit
h : J.snd l = r'
⊢ left l ⟶ right r'

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker
⊢ f ≫ g = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (moduleCatMkOfKerLERange f g ⋯).Exact

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ ModuleCat.ofHom (ModuleCat.Hom.hom S.g).ker.subtype ≫ S.g = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (ModuleCat.kernelIsLimit S.g).lift (KernelFork.ofι S.f ⋯) ≫ ModuleCat.ofHom S.moduleCatToCycles.range.mkQ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.toCycles ≫ S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f'

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.pOpcycles ≫ S.moduleCatOpcyclesIso.hom = ModuleCat.ofHom (ModuleCat.Hom.hom S.f).range.mkQ

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
⊢ ∀ (X Y : WalkingMultispan J), Small.{t, max w w'} (X ⟶ Y)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
x y : ↑S.X₂
h : (ConcreteCategory.hom S.pOpcycles) x = (ConcreteCategory.hom S.pOpcycles) y
⊢ Submodule.Quotient.mk x = Submodule.Quotient.mk y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
x y : ↑S.X₂
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
⊢ (ConcreteCategory.hom S.moduleCatOpcyclesIso.hom) ((ConcreteCategory.hom S.pOpcycles) x) =
    (ConcreteCategory.hom S.moduleCatOpcyclesIso.hom) ((ConcreteCategory.hom S.pOpcycles) y)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
x : ↑S.X₂
⊢ (ConcreteCategory.hom S.pOpcycles) x = 0 ↔ x ∈ (ModuleCat.Hom.hom S.f).range

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles

Tactic:
by

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
f : M →ₗ[R] N
⊢ ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f = 0

Tactic:
by

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
f : M →ₗ[R] N
h : Function.Surjective ⇑f
x✝ : ↑f.shortComplexKer.X₂
⊢ (ConcreteCategory.hom f.shortComplexKer.g) x✝ = 0 ↔ x✝ ∈ Set.range ⇑(ConcreteCategory.hom f.shortComplexKer.f)

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
⊢ Function.LeftInverse
    (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)

Tactic:
by

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

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

Goal state before:
pp: J : MultispanShape
⊢ Function.RightInverse
    (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)

Tactic:
by

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 v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁

Tactic:
by

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'
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑((↑eN.symm ∘ₗ f) ∘ₗ ↑eM) ⇑(↑eL.symm ∘ₗ g ∘ₗ ↑eN)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
⊢ ∀ (X : WalkingMulticospan J),
    (match X, X, 𝟙 X 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 X with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)

Tactic:
by

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 v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
e : forget₂ C Ab ⋙ forget Ab ≅ forget C
⊢ (ConcreteCategory.hom ((forget₂ C Ab ⋙ forget Ab).map D.L₁.g ≫ e.hom.app D.L₁.X₃)) x₂ =
    (ConcreteCategory.hom ((forget₂ C Ab ⋙ forget Ab).map D.v₀₁.τ₃ ≫ e.hom.app D.L₁.X₃)) x₃

Tactic:
by

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'
exact : Function.Exact ⇑f ⇑g
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑g
⊢ (shortComplexOfConj eM eN eL f g ⋯).ShortExact

Tactic:
by

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 v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
e : forget₂ C Ab ⋙ forget Ab ≅ forget C
⊢ (ConcreteCategory.hom ((forget₂ C Ab ⋙ forget Ab).map D.L₂.f ≫ e.hom.app D.L₂.X₂)) x₁ =
    (ConcreteCategory.hom ((forget₂ C Ab ⋙ forget Ab).map D.v₁₂.τ₂ ≫ e.hom.app D.L₂.X₂)) x₂

Tactic:
by

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 v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map D.δ)) x₃ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₂₃.τ₁)) x₁

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
S : ShortComplex (ModuleCat R')
h : S.Exact
⊢ (S.map (restrictScalars f)).Exact

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
⊢ Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
⊢ Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
⊢ ∀ {X Y Z : WalkingMulticospan J} (f : X ⟶ Y) (g : Y ⟶ Z),
    (match X, Z, f ≫ g 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 X, Y, f 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 Y, Z, g 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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
d : Fan I.right
hd : IsLimit d
i : J.R
⊢ I.fstPiMapOfIsLimit c hd ≫ d.proj i = c.proj (J.fst i) ≫ I.fst i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
d : Fan I.right
hd : IsLimit d
i : J.R
⊢ I.sndPiMapOfIsLimit c hd ≫ d.proj i = c.proj (J.snd i) ≫ I.snd i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
⊢ ∀ (X : WalkingMultispan J),
    (match X, X, 𝟙 X 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 X with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ∀ ⦃X Y : Discrete WalkingPair⦄ (f : X ⟶ Y),
    (((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map f ≫
        Discrete.casesOn Y fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) =
      (Discrete.casesOn X fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N))) ≫
        (pair M N).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
⊢ ∀ {X Y Z : WalkingMultispan J} (f : X ⟶ Y) (g : Y ⟶ Z),
    (match X, Z, f ≫ g 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 X, Y, f 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 Y, Z, g 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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
d : Cofan I.right
hc : IsColimit c
i : J.L
⊢ c.inj i ≫ I.fstSigmaMapOfIsColimit d hc = I.fst i ≫ d.inj (J.fst i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
d : Cofan I.right
hc : IsColimit c
i : J.L
⊢ c.inj i ≫ I.sndSigmaMapOfIsColimit d hc = I.snd i ≫ d.inj (J.snd i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.fst b) ≫ I.fst b

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ∀ (s : Cone (pair M N)) (j : Discrete WalkingPair),
    ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b

Tactic:
by

Goal state after: