mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ (mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11
      mono_of_epi_of_mono_of_mono'._proof_7 =
    0

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ (mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11
      mono_of_epi_of_mono_of_mono'._proof_7 =
    0
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inl S₁.f).v (n + 1) n ⋯ ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inl S₁.f).v (n + 1) n ⋯ ≫ (descShortComplex S₁ ≫ f.τ₃).f n

pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inr S₁.f).f n ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inr S₁.f).f n ≫ (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
·

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inl S₁.f).v (n + 1) n ⋯ ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inl S₁.f).v (n + 1) n ⋯ ≫ (descShortComplex S₁ ≫ f.τ₃).f n
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inr S₁.f).f n ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inr S₁.f).f n ≫ (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
·

Goal state after:
case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inr S₁.f).f n ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inr S₁.f).f n ≫ (descShortComplex S₁ ≫ f.τ₃).f n
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₁ + b₂ = b₃

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).Exact

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).Exact

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).Exact
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.Exact

Tactic:
·

Goal state after:
case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) opShiftFunctorEquivalence_unitIso_hom_app._auto_1
⊢ m + n = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) opShiftFunctorEquivalence_unitIso_inv_app._auto_1
⊢ m + n = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : autoParam (m + n = p) opShiftFunctorEquivalence_add_unitIso_hom_app_eq._auto_1
⊢ n + m = p

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ n + m = p

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.Exact

Tactic:
·

Goal state after:
case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.Exact
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).Exact

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).Exact
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

pp: case refine_2.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.Exact

Tactic:
·

Goal state after:
case refine_2.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : autoParam (m + n = p) opShiftFunctorEquivalence_add_unitIso_inv_app_eq._auto_1
⊢ n + m = p

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) shiftFunctorCompIsoId_op_hom_app._auto_1
⊢ m + n = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ m + n = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.Exact

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.Exact
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
m n : ℤ
hmn : m + n = 0
⊢ m = -n

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ n + -n = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).Exact

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).Exact
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ a + b = c

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

Tactic:
·

Goal state after:
case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact