awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₂ : Epi (app' φ (k₀ + 2) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
⊢ Epi (app' φ (k₀ + 1) ⋯)
have h₁ : Epi (X := R₁.obj' (k₀ + 0) sorry) (app' φ (k₀ + 0) sorry)
Tactic: change Epi (app' φ (k₀ + 0)) at h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₂ : Epi (app' φ (k₀ + 2) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
h₀ : Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)
⊢ Epi (app' φ (k₀ + 1) ⋯)
have rw : ∀
  (h₂ :
    Epi (X := R₁.obj' (k₀ + 2) sorry) (Y := R₂.obj' (k₀ + 2) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 2 mono_of_epi_of_mono_of_mono'._proof_4 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 2 mono_of_epi_of_mono_of_mono'._proof_4 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 2 mono_of_epi_of_mono_of_mono'._proof_4))
  (h₃ :
    Mono (X := R₁.obj' (k₀ + 3) sorry) (Y := R₂.obj' (k₀ + 3) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 3 mono_of_epi_of_mono_of_mono'._proof_7 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 3 mono_of_epi_of_mono_of_mono'._proof_7 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 3 mono_of_epi_of_mono_of_mono'._proof_7))
  (h₀ :
    Epi (X := R₁.obj' (k₀ + 0) sorry) (Y := R₂.obj' (k₀ + 0) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 0 mono_of_epi_of_mono_of_mono'._proof_13 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 0 mono_of_epi_of_mono_of_mono'._proof_13)),
  Epi (X := R₁.obj' (k₀ + 1) sorry) (Y := R₂.obj' (k₀ + 1) sorry)
    (app' (Functor.map (natAddLEFunctor h) φ) 1 mono_of_epi_of_mono_of_mono'._proof_11 :
      (Functor.obj (natAddLEFunctor h) R₁).obj' 1 mono_of_epi_of_mono_of_mono'._proof_11 ⟶
        (Functor.obj (natAddLEFunctor h) R₂).obj' 1 mono_of_epi_of_mono_of_mono'._proof_11)
Tactic: rw [← natAddLEFunctor_app' h] at h₀ h₂ h₃ ⊢
Cleared hypotheses: h₂, h₃, h₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n k : ℕ
h : k + 4 ≤ n
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ k₄ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
hk₄ : k₄ = k + 4
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₁ : IsIso (X := R₁.obj' k₁ ⋯) (app' φ k₁ ⋯)
h₃ : IsIso (X := R₁.obj' k₃ ⋯) (app' φ k₃ ⋯)
h₄ : Mono (X := R₁.obj' k₄ ⋯) (app' φ k₄ ⋯)
⊢ IsIso (X := R₁.obj' k₂ ⋯) (app' φ k₂ ⋯)
have subst_vars : ∀ (h : k₀ + 4 ≤ n) (h₀ : Epi (X := R₁.obj' k₀ sorry) (app' φ k₀ sorry)) (h₁ : IsIso (app' φ (k₀ + 1) sorry))
  (h₃ : IsIso (app' φ (k₀ + 3) sorry)) (h₄ : Mono (app' φ (k₀ + 4) sorry)), IsIso (app' φ (k₀ + 2) sorry)
Tactic: subst_vars
Cleared hypotheses: k, h, k₁, k₂, k₃, k₄, hk₀, hk₁, hk₂, hk₃, hk₄, h₀, h₁, h₃, h₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 4 ≤ n
h₀ : Epi (X := R₁.obj' k₀ ⋯) (app' φ k₀ ⋯)
h₁ : IsIso (app' φ (k₀ + 1) ⋯)
h₃ : IsIso (app' φ (k₀ + 3) ⋯)
h₄ : Mono (app' φ (k₀ + 4) ⋯)
⊢ IsIso (app' φ (k₀ + 2) ⋯)
have h₂ : Epi (X := R₁.obj' (k₀ + 0) sorry) (app' φ (k₀ + 0) sorry)
Tactic: change Epi (app' φ (k₀ + 0)) at h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℕ
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 4 ≤ n
h₁ : IsIso (app' φ (k₀ + 1) ⋯)
h₃ : IsIso (app' φ (k₀ + 3) ⋯)
h₄ : Mono (app' φ (k₀ + 4) ⋯)
h₀ : Epi (X := R₁.obj' (k₀ + 0) ⋯) (app' φ (k₀ + 0) ⋯)
⊢ IsIso (app' φ (k₀ + 2) ⋯)
have rw : ∀
  (h₁ :
    IsIso (X := R₁.obj' (k₀ + 1) sorry) (Y := R₂.obj' (k₀ + 1) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4))
  (h₃ :
    IsIso (X := R₁.obj' (k₀ + 3) sorry) (Y := R₂.obj' (k₀ + 3) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6))
  (h₄ :
    Mono (X := R₁.obj' (k₀ + 4) sorry) (Y := R₂.obj' (k₀ + 4) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7))
  (h₀ :
    Epi (X := R₁.obj' (k₀ + 0) sorry) (Y := R₂.obj' (k₀ + 0) sorry)
      (app' (Functor.map (natAddLEFunctor h) φ) 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2 :
        (Functor.obj (natAddLEFunctor h) R₁).obj' 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2 ⟶
          (Functor.obj (natAddLEFunctor h) R₂).obj' 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)),
  IsIso (X := R₁.obj' (k₀ + 2) sorry) (Y := R₂.obj' (k₀ + 2) sorry)
    (app' (Functor.map (natAddLEFunctor h) φ) 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9 :
      (Functor.obj (natAddLEFunctor h) R₁).obj' 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9 ⟶
        (Functor.obj (natAddLEFunctor h) R₂).obj' 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)
Tactic: rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ h₄ ⊢
Cleared hypotheses: h₁, h₃, h₄, h₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := R₁.obj' 0 ⋯)
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ : R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    0 ⟶
  mk₃ (X₀ := R₂.obj ⟨0, ⋯⟩) (X₁ := R₂.obj ⟨1, ⋯⟩) (X₃ := R₁.obj' 0 ⋯)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯)
    (𝟙
      ((mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ :=
            R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₃ := R₁.obj' 0 ⋯)
            (R₁.map' 0 1 ⋯ ⋯ :
              R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 ⋯ ⋯ :
              R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            0).obj'
        3 _proof_300✝))
    ⋯ ⋯ ⋯
⊢ Mono (app' ψ 3 mono_of_epi_of_mono_of_mono'._proof_7)
have dsimp : Mono.{v_1, u_1}
  (𝟙
    (Precomp.obj
      (mk₂ (X₀ := R₁.obj 1) (X₁ := R₁.obj 2) (X₂ := R₁.obj 0) (R₁.map (homOfLE sorry) : R₁.obj 1 ⟶ R₁.obj 2)
        (0 : R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj' 0 sorry))
      (R₁.obj 0) 3))
Tactic: dsimp [ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := R₁.obj' 0 ⋯)
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ : R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    0 ⟶
  mk₃ (X₀ := R₂.obj ⟨0, ⋯⟩) (X₁ := R₂.obj ⟨1, ⋯⟩) (X₃ := R₁.obj' 0 ⋯)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯)
    (𝟙
      ((mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ :=
            R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₃ := R₁.obj' 0 ⋯)
            (R₁.map' 0 1 ⋯ ⋯ :
              R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 ⋯ ⋯ :
              R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            0).obj'
        3 _proof_300✝))
    ⋯ ⋯ ⋯
⊢ Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
have refine_1 : (mk₃ (X₀ := R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
        (X₃ := R₁.obj' 0 sorry)
        (R₁.map' 0 1 sorry sorry :
          R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
        (R₁.map' 1 2 sorry sorry :
          R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
        0).map'
    0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 =
  0
Tactic: refine mono_of_epi_of_mono_of_mono' ψ ?_ (exact₂_mk _ (by simp) ?_)
    (hR₂.exact 0).exact_toComposableArrows h₀ h₁ (by dsimp [ψ]; infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} 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₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
    R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (0 : R₁.obj' 0 ⋯ ⟶ R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ :
      R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) ⟶
  mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₂.obj ⟨0, ⋯⟩) (X₂ := R₂.obj ⟨1, ⋯⟩) (0 : R₁.obj' 0 ⋯ ⟶ R₂.obj ⟨0, ⋯⟩)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) :=
  homMk₃
    (𝟙
      ((mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
            R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (0 : R₁.obj' 0 ⋯ ⟶ R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 0 1 ⋯ ⋯ :
              R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 ⋯ ⋯ :
              R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).obj'
        0 _proof_297✝))
    (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯
⊢ Epi (app' ψ 0 mono_of_epi_of_mono_of_mono'._proof_13)
have dsimp : Epi.{v_1, u_1} (𝟙 (R₁.obj 0))
Tactic: dsimp [ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} C 2
φ : R₁ ⟶ R₂
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)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
    R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (0 : R₁.obj' 0 ⋯ ⟶ R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ :
      R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) ⟶
  mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₂.obj ⟨0, ⋯⟩) (X₂ := R₂.obj ⟨1, ⋯⟩) (0 : R₁.obj' 0 ⋯ ⟶ R₂.obj ⟨0, ⋯⟩)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) :=
  homMk₃
    (𝟙
      ((mk₃ (X₀ := R₁.obj' 0 ⋯) (X₁ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₂ :=
            R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (0 : R₁.obj' 0 ⋯ ⟶ R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 0 1 ⋯ ⋯ :
              R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 ⋯ ⋯ :
              R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).obj'
        0 _proof_297✝))
    (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯
⊢ Epi (app' ψ 0 mono_of_epi_of_mono_of_mono'._proof_13)
have dsimp : Epi.{v_1, u_1} (𝟙 (R₁.obj 0))
Tactic: dsimp [ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} C 2
φ : R₁ ⟶ R₂
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)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := R₁.obj' 0 ⋯)
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ : R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    0 ⟶
  mk₃ (X₀ := R₂.obj ⟨0, ⋯⟩) (X₁ := R₂.obj ⟨1, ⋯⟩) (X₃ := R₁.obj' 0 ⋯)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯)
    (𝟙
      ((mk₃ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ :=
            R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₃ := R₁.obj' 0 ⋯)
            (R₁.map' 0 1 ⋯ ⋯ :
              R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            (R₁.map' 1 2 ⋯ ⋯ :
              R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
            0).obj'
        3 _proof_300✝))
    ⋯ ⋯ ⋯
⊢ Mono (app' ψ 3 mono_of_epi_of_mono_of_mono'._proof_7)
have dsimp : Mono.{v_1, u_1}
  (𝟙
    (Precomp.obj
      (mk₂ (X₀ := R₁.obj 1) (X₁ := R₁.obj 2) (X₂ := R₁.obj 0) (R₁.map (homOfLE sorry) : R₁.obj 1 ⟶ R₁.obj 2)
        (0 : R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj' 0 sorry))
      (R₁.obj 0) 3))
Tactic: dsimp [ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} 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₄ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := 0) (X₄ := 0)
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ : R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    0 0 ⟶
  mk₄ (X₀ := R₂.obj ⟨0, ⋯⟩) (X₁ := R₂.obj ⟨1, ⋯⟩) (X₃ := 0) (X₄ := 0)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ IsIso (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
have refine_1 : (mk₄ (X₀ := R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := 0) (X₄ := 0)
    (R₁.map' 0 1 sorry sorry : R₁.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 sorry sorry : R₁.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    0 0).Exact
Tactic: refine isIso_of_epi_of_isIso_of_isIso_of_mono ?_ ?_ ψ h₀ h₁ inferInstance inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
R₁ R₂ : ComposableArrows.{v_1, u_1} 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₄ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := 0) (X₄ := 0)
    (R₁.map' 0 1 ⋯ ⋯ : R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₁.map' 1 2 ⋯ ⋯ : R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    0 0 ⟶
  mk₄ (X₀ := R₂.obj ⟨0, ⋯⟩) (X₁ := R₂.obj ⟨1, ⋯⟩) (X₃ := 0) (X₄ := 0)
    (R₂.map' 0 1 ⋯ ⋯ : R₂.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨1, ⋯⟩)
    (R₂.map' 1 2 ⋯ ⋯ : R₂.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj ⟨2, ⋯⟩) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
refine_1 :
  (mk₄ (X₀ := R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
      (X₃ := 0) (X₄ := 0)
      (R₁.map' 0 1 ⋯ ⋯ :
        R₁.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
      (R₁.map' 1 2 ⋯ ⋯ :
        R₁.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₁.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
      0 0).Exact
⊢ IsIso (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
have refine_2 : (mk₄ (X₀ := R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (X₃ := 0) (X₄ := 0)
    (R₂.map' 0 1 sorry sorry : R₂.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    (R₂.map' 1 2 sorry sorry : R₂.obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ R₂.obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
    0 0).Exact
Tactic: refine isIso_of_epi_of_isIso_of_isIso_of_mono ?_ ?_ ψ h₀ h₁ inferInstance inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := biprod.{v, u} X Y ⟶ Z) (φ f g ≫ biprod.snd) (biprod.snd ≫ g)
have dsimp : Eq (α := biprod.{v, u} X Y ⟶ Z)
  (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g)) biprod.snd)
  (biprod.snd ≫ g)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := kernel (f ≫ g) ⟶ biprod.{v, u} Y Z) (ι f g ≫ φ f g) 0
have dsimp : Eq (α := kernel (f ≫ g) ⟶ biprod.{v, u} Y Z)
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) (biprod.lift (kernel.ι (f ≫ g)) (kernel.ι (f ≫ g) ≫ f))
    (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g)))
  0
Tactic: dsimp [ι, φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := biprod.{v, u} X Y ⟶ cokernel (f ≫ g)) (φ f g ≫ π f g) 0
have dsimp : Eq (α := biprod.{v, u} X Y ⟶ cokernel (f ≫ g))
  (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
    (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g))))
  0
Tactic: dsimp [φ, π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := biprod.{v, u} X Y ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
      (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g))))
    0
have h₀ : Eq (α := X ⟶ cokernel (f ≫ g))
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
      (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)))))
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₀ :
  Eq (α := X ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
        (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)))))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl 0)
⊢ Eq (α := biprod.{v, u} X Y ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
      (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g))))
    0
have h₁ : Eq (α := Y ⟶ cokernel (f ≫ g))
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
      (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)))))
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr 0)
Tactic: ext