mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
·

Goal state after:
case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.right.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).IsComplex

pp: case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).sc' ?mp.right.hS 0 1 2 exact₂_iff._proof_2
      exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

Tactic:
·

Goal state after:
case mp.right.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).IsComplex
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ n + 2 ≤ n + 2

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact → S.Exact

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact → S.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

pp: case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact

Tactic:
·

Goal state after:
case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_1.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝¹ : i + 2 ≤ n + 2
hi✝ : i ≤ n
hi : i < n
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝¹ = 0

pp: case mpr.refine_1.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝ = 0

Tactic:
·

Goal state after:
case mpr.refine_1.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝¹ : i + 2 ≤ n + 2
hi✝ : i ≤ n
hi : i < n
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝¹ = 0
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_1.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝ = 0

Tactic:
·

Goal state after:
case mpr.refine_1.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi✝ = 0
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact

Tactic:
·

Goal state after:
case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝¹ : i + 2 ≤ n + 2
hi✝ : i ≤ n
hi : i < n
⊢ (S.sc ⋯ i hi✝¹).Exact

pp: case mpr.refine_2.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ (S.sc ⋯ i hi✝).Exact

Tactic:
·

Goal state after:
case mpr.refine_2.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝¹ : i + 2 ≤ n + 2
hi✝ : i ≤ n
hi : i < n
⊢ (S.sc ⋯ i hi✝¹).Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ (S.sc ⋯ i hi✝).Exact

Tactic:
·

Goal state after:
case mpr.refine_2.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ (S.sc ⋯ i hi✝).Exact
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ) →
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ) →
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y), (sum g fun g' t ↦ single (a ≫ g') (0 * t)) = 0

Tactic:
·

Goal state after:
case h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y), (sum g fun g' t ↦ single (a ≫ g') (0 * t)) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun g' t ↦ single (a ≫ g') ((b₁ + b₂) * t)) =
      (sum g fun g' t ↦ single (a ≫ g') (b₁ * t)) + sum g fun g' t ↦ single (a ≫ g') (b₂ * t)

Tactic:
·

Goal state after:
case h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun g' t ↦ single (a ≫ g') ((b₁ + b₂) * t)) =
      (sum g fun g' t ↦ single (a ≫ g') (b₁ * t)) + sum g fun g' t ↦ single (a ≫ g') (b₂ * t)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g.h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z), single (r ≫ a) (h * 0) = 0

Tactic:
·

Goal state after:
case e_g.h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z), single (r ≫ a) (h * 0) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g.h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), single (r ≫ a) (h * (b₁ + b₂)) = single (r ≫ a) (h * b₁) + single (r ≫ a) (h * b₂)

Tactic:
·

Goal state after:
case e_g.h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), single (r ≫ a) (h * (b₁ + b₂)) = single (r ≫ a) (h * b₁) + single (r ≫ a) (h * b₂)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum f fun i a ↦ sum g fun g' t ↦ single (i ≫ g') (r * a * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
simp [Finsupp.smul_sum, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (i : X ⟶ Y), (sum g fun g' t ↦ single (i ≫ g') (0 * t)) = 0

Tactic:
simp [Finsupp.smul_sum, mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Y), 0 • F.map a = 0

pp: case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

pp: case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

pp: case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
·

Goal state after:
case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Y), 0 • F.map a = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

pp: case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

pp: case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
·

Goal state after:
case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

pp: case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
·

Goal state after:
case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
·

Goal state after:
case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : Y ⟶ Z), 0 • F.map a = 0

pp: case single.add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

pp: case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

pp: case single.add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
·

Goal state after:
case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : Y ⟶ Z), 0 • F.map a = 0