awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (y₁ : A₁ ⟶ S.L₁.X₁) (hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
Tactic: obtain ⟨A₁, π₁, hπ₁, y₁, hy₁⟩ := S.L₁_exact.exact_up_to_refinements (x₂ ≫ S.v₀₁.τ₂)
    (by rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
have hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
Tactic: have hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0 := by
    simp only [← cancel_mono S.L₂.f, assoc, zero_comp, S.v₁₂.comm₁₂,
      ← reassoc_of% hy₁, w₀₂_τ₂, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
have obtain : ∀ (x₁ : A₁ ⟶ S.L₀.X₁) (hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
Tactic: obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S.v₀₁.τ₁ = y₁ := ⟨_, S.exact_C₁_up.lift_f y₁ hy₁'⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
x₁ : A₁ ⟶ S.L₀.X₁
hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
have refine : π₁ ≫ x₂ = x₁ ≫ S.L₀.f
Tactic: refine ⟨A₁, π₁, hπ₁, x₁, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ S.L₀'.f ≫ S.φ₁ = S.v₁₂.τ₁
have dsimp : pullback.lift S.L₁.f 0 sorry ≫ S.φ₁ = S.v₁₂.τ₁
Tactic: dsimp only [L₀']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Epi S.L₀'.g
have dsimp : Epi (X := S.P) (pullback.snd S.L₁.g S.v₀₁.τ₃)
Tactic: dsimp only [L₀']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ S.L₀'.Exact
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀'.X₂),
  x₂ ≫ S.L₀'.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀'.X₁), π ≫ x₂ = x₁ ≫ S.L₀'.f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
⊢ (x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃) ≫ S.L₁.g = 0
have rw : x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.L₁.g = 0
Tactic: rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
rw : x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.L₁.g = 0
⊢ (x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃) ≫ S.L₁.g = 0
have rw₁ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.v₀₁.τ₃ = 0
Tactic: rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
rw : x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.L₁.g = 0
rw₁ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.v₀₁.τ₃ = 0
⊢ (x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃) ≫ S.L₁.g = 0
have rw₂ : Eq (α := A ⟶ S.L₁.X₃) (0 ≫ S.v₀₁.τ₃) 0
Tactic: rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
rw : x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.L₁.g = 0
rw₁ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.v₀₁.τ₃ = 0
rw₂ : Eq (α := A ⟶ S.L₁.X₃) (0 ≫ S.v₀₁.τ₃) 0
⊢ (x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃) ≫ S.L₁.g = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S.L₁.X₃) 0 0
Tactic: rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀'.X₁), π ≫ x₂ = x₁ ≫ S.L₀'.f
have obtain : ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (x₁ : A' ⟶ S.L₁.X₁) (fac : π ≫ x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = x₁ ≫ S.L₁.f),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀'.X₁), π ≫ x₂ = x₁ ≫ S.L₀'.f
Tactic: obtain ⟨A', π, hπ, x₁, fac⟩ := S.L₁_exact.exact_up_to_refinements (x₂ ≫ pullback.fst _ _)
    (by rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ S.L₀.g ≫ S.δ = 0
have rw : (S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃) ≫ S.δ = 0
Tactic: rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃) ≫ S.δ = 0
⊢ S.L₀.g ≫ S.δ = 0
have rw₁ : S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
Tactic: rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃) ≫ S.δ = 0
rw₁ : S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
⊢ S.L₀.g ≫ S.δ = 0
have rw₂ : S.L₀X₂ToP ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
Tactic: rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃) ≫ S.δ = 0
rw₁ : S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
rw₂ : S.L₀X₂ToP ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
⊢ S.L₀.g ≫ S.δ = 0
have rw₃ : Eq (α := S.L₀.X₂ ⟶ S.L₃.X₁) (0 ≫ S.v₂₃.τ₁) 0
Tactic: rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃) ≫ S.δ = 0
rw₁ : S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
rw₂ : S.L₀X₂ToP ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
rw₃ : Eq (α := S.L₀.X₂ ⟶ S.L₃.X₁) (0 ≫ S.v₂₃.τ₁) 0
⊢ S.L₀.g ≫ S.δ = 0
have rw₄ : Eq.{v_1 + 1} (α := S.L₀.X₂ ⟶ S.L₃.X₁) 0 0
Tactic: rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ S.L₁'.Exact
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂),
  x₂ ≫ S.L₁'.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₂ = x₁ ≫ S.L₁'.f
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
have obtain : ∀ (A₁ : C) (π₁ : A₁ ⟶ A₀) (hπ₁ : Epi π₁) (p : A₁ ⟶ S.L₀'.X₂) (hp : π₁ ≫ x₃ = p ≫ S.L₀'.g),
  ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
Tactic: obtain ⟨A₁, π₁, hπ₁, p, hp⟩ := surjective_up_to_refinements_of_epi S.L₀'.g x₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
have rw : p ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
Tactic: rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
rw : p ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
have rw₁ : p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
Tactic: rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
rw : p ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
rw₁ : p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
have rw₂ : π₁ ≫ x₃ ≫ S.δ = 0
Tactic: rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
rw : p ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
rw₁ : p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
rw₂ : π₁ ≫ x₃ ≫ S.δ = 0
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
have rw₃ : Eq (α := A₁ ⟶ S.L₃.X₁) (π₁ ≫ 0) 0
Tactic: rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
rw : p ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
rw₁ : p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
rw₂ : π₁ ≫ x₃ ≫ S.δ = 0
rw₃ : Eq (α := A₁ ⟶ S.L₃.X₁) (π₁ ≫ 0) 0
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
have rw₄ : Eq.{v_1 + 1} (α := A₁ ⟶ S.L₃.X₁) 0 0
Tactic: rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
have hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
Tactic: have hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0 := by
    rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
have obtain : ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂)
  (x₁ :
    A₂ ⟶
      { X₁ := S.L₁.X₁, X₂ := S.L₂.X₁, X₃ := S.L₃.X₁, f := S.v₁₂.τ₁, g := S.v₂₃.τ₁, zero := sorry :
          ShortComplex.{v_1, u_1} C }.X₁)
  (hx₁ :
    π₂ ≫ p ≫ S.φ₁ = x₁ ≫ { X₁ := S.L₁.X₁, X₂ := S.L₂.X₁, X₃ := S.L₃.X₁, f := S.v₁₂.τ₁, g := S.v₂₃.τ₁, zero := sorry }.f),
  ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
Tactic: obtain ⟨A₂, π₂, hπ₂, x₁, hx₁⟩ := S.exact_C₁_down.exact_up_to_refinements (p ≫ S.φ₁) hp'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
have hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0
Tactic: have hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0 := by
    simp only [x₂, x₂', sub_comp, assoc, ← S.v₁₂.comm₁₂, ← reassoc_of% hx₁, φ₂, φ₁_L₂_f, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0
k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
have hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂'
Tactic: have hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂' := S.exact_C₂_up.lift_f _ _
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0
k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'
hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂'
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
have hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
Tactic: have hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd _ _ := by
    simp only [x₂, x₂', ← cancel_mono S.v₀₁.τ₃, assoc, ← S.v₀₁.comm₂₃, reassoc_of% hk₂,
      sub_comp, S.L₁.zero, comp_zero, sub_zero, pullback.condition]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ S.op.δ.unop = S.δ.op.unop
have rw : Eq (α := Opposite.unop S.op.P' ⟶ Opposite.unop S.op.P)
  (Quiver.Hom.unop (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op) ≫
    S.op.δ.unop ≫ Quiver.Hom.unop (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op))
  (CategoryStruct.comp (Y := S.L₁.X₂)
    (Quiver.Hom.unop (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op) :
      Opposite.unop
          (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃) S.L₁.g.op
            S.v₀₁.τ₃.op) ⟶
        Opposite.unop (Opposite.op S.L₁.X₂))
    (S.v₁₂.τ₂ ≫ Quiver.Hom.unop (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op)))
Tactic: rw [Quiver.Hom.unop_op, ← cancel_mono (pushout.inr _ _ : _ ⟶ S.P'),
    ← cancel_epi (pullback.snd _ _ : S.P ⟶ _), S.snd_δ_inr,
    ← cancel_mono S.P'IsoUnopOpP.hom, ← cancel_epi S.PIsoUnopOpP'.inv,
    P'IsoUnopOpP, PIsoUnopOpP', assoc, assoc, assoc, assoc,
    pushoutIsoUnopPullback_inr_hom, pullbackIsoUnopPushout_inv_snd_assoc,
    pushoutIsoUnopPullback_inl_hom, pullbackIsoUnopPushout_inv_fst_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Eq (α := Opposite.unop S.op.P' ⟶ Opposite.unop S.op.P)
    (Quiver.Hom.unop (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op) ≫
      S.op.δ.unop ≫ Quiver.Hom.unop (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op))
    (CategoryStruct.comp (Y := S.L₁.X₂)
      (Quiver.Hom.unop (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op) :
        Opposite.unop
            (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃)
              S.L₁.g.op S.v₀₁.τ₃.op) ⟶
          Opposite.unop (Opposite.op S.L₁.X₂))
      (S.v₁₂.τ₂ ≫ Quiver.Hom.unop (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op)))
have a : Eq (α :=
  Opposite.op (Opposite.unop S.op.P) ⟶
    Opposite.op
      (Opposite.unop
        (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃) S.L₁.g.op
          S.v₀₁.τ₃.op)))
  (Quiver.Hom.op
    (Quiver.Hom.unop (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op) ≫
      S.op.δ.unop ≫ Quiver.Hom.unop (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op)))
  (Quiver.Hom.op
    (CategoryStruct.comp (Y := S.L₁.X₂)
      (Quiver.Hom.unop (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op) :
        Opposite.unop
            (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃)
              S.L₁.g.op S.v₀₁.τ₃.op) ⟶
          Opposite.unop (Opposite.op S.L₁.X₂))
      (S.v₁₂.τ₂ ≫ Quiver.Hom.unop (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op))))
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Iso.hom (Iso.refl S.L₂'.op.X₂) ≫ S.op.L₁'.g = S.L₂'.op.g ≫ Iso.hom (Iso.refl S.L₂'.op.X₃)
have dsimp : 𝟙 (Opposite.op S.L₃.X₁) ≫ S.op.δ = S.δ.op ≫ 𝟙 (Opposite.op S.L₀.X₃)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ S.L₂'.Exact
have rw : S.op.L₁'.Exact
Tactic: rw [← exact_op_iff, exact_iff_of_iso S.L₂'OpIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
have H : CategoryStruct.comp (Y := pullback S.L₁.g S.v₀₁.τ₃) (pullback.lift x₂ x₃ h₂) (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ) =
  pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
Tactic: have H := (pullback.lift x₂ x₃ h₂) ≫= S.snd_δ
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H :
  CategoryStruct.comp (Y := pullback S.L₁.g S.v₀₁.τ₃) (pullback.lift x₂ x₃ h₂) (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ) =
    pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
have H₁ : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
Tactic: rw [pullback.lift_snd_assoc] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
have rw : (pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁
Tactic: rw [H, ← assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ (pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁
have e_a : pullback.lift x₂ x₃ h₂ ≫ S.φ₁ = x₁
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S S₁ S₂ S₃ x : SnakeInput.{v_1, u_1} C
⊢ pullback.map x.L₁.g x.v₀₁.τ₃ x.L₁.g x.v₀₁.τ₃ (Hom.f₁ (𝟙 x)).τ₂ (Hom.f₀ (𝟙 x)).τ₃ (Hom.f₁ (𝟙 x)).τ₃ ⋯ ⋯ = 𝟙 x.P
have dsimp : pullback.map x.L₁.g x.v₀₁.τ₃ x.L₁.g x.v₀₁.τ₃ (𝟙 x.L₁.X₂) (𝟙 x.L₀.X₃) (𝟙 x.L₁.X₃) sorry sorry = 𝟙 (pullback x.L₁.g x.v₀₁.τ₃)
Tactic: dsimp [P]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S S₁ S₂ S₃ X Y Z : SnakeInput.{v_1, u_1} C
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := X.P ⟶ Z.P) (pullback.map X.L₁.g X.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ (x ≫ x_1).f₁.τ₂ (x ≫ x_1).f₀.τ₃ (x ≫ x_1).f₁.τ₃ ⋯ ⋯)
    (CategoryStruct.comp (Y := Y.P) (pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ x.f₁.τ₂ x.f₀.τ₃ x.f₁.τ₃ ⋯ ⋯)
      (pullback.map Y.L₁.g Y.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ x_1.f₁.τ₂ x_1.f₀.τ₃ x_1.f₁.τ₃ ⋯ ⋯))
have dsimp : Eq (α := pullback X.L₁.g X.v₀₁.τ₃ ⟶ pullback Z.L₁.g Z.v₀₁.τ₃)
  (pullback.map X.L₁.g X.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ (x.f₁.τ₂ ≫ x_1.f₁.τ₂) (x.f₀.τ₃ ≫ x_1.f₀.τ₃) (x.f₁.τ₃ ≫ x_1.f₁.τ₃) sorry sorry)
  (CategoryStruct.comp (Y := pullback Y.L₁.g Y.v₀₁.τ₃)
    (pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ x.f₁.τ₂ x.f₀.τ₃ x.f₁.τ₃ sorry sorry)
    (pullback.map Y.L₁.g Y.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ x_1.f₁.τ₂ x_1.f₀.τ₃ x_1.f₁.τ₃ sorry sorry))
Tactic: dsimp [P]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
⊢ S₁.φ₂ ≫ f.f₂.τ₂ = Functor.map functorP f ≫ S₂.φ₂
have dsimp : Eq (α := S₁.P ⟶ S₂.L₂.X₂) ((pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂)
  (CategoryStruct.comp (Y := S₂.P) (pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ sorry sorry)
    (pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂))
Tactic: dsimp [φ₂]