awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
pos :
  ∀ (hij : c.Rel i j),
    Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (if hij : c.Rel i j then
          if hi : e.BoundaryGE i then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else 0)
        (if hij : c.Rel j k then
          if hi : e.BoundaryGE j then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else 0))
      0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have neg : ∀ (hij : ¬c.Rel i j),
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
      else 0))
    0
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have pos : ∀ (hjk : c.Rel j k),
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
      else 0))
    0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
pos :
  ∀ (hjk : c.Rel j k),
    Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (if hij : c.Rel i j then
          if hi : e.BoundaryGE i then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else 0)
        (if hij : c.Rel j k then
          if hi : e.BoundaryGE j then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else 0))
      0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have neg : ∀ (hjk : ¬c.Rel j k),
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
      else 0))
    0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have pos : Eq (α := X K e i ⟶ X K e k)
  (CategoryStruct.comp (Y := X K e j)
    (if hi : e.BoundaryGE i then Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
    else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry))
    (Iso.hom (XIso K e sorry) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)))
  0
Tactic: rw [dif_pos hij, dif_pos hjk, dif_neg (e.not_boundaryGE_next hij)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hi : e.BoundaryGE i then Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
      (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
    0
have pos : ∀ (h : e.BoundaryGE i),
  Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (Iso.hom (XIsoOpcycles K e h) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry))
      (Iso.hom (XIso K e sorry) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)))
    0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
pos :
  ∀ (h : e.BoundaryGE i),
    Eq (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (Iso.hom (XIsoOpcycles K e h) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
        (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
      0
⊢ Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hi : e.BoundaryGE i then Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
      (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
    0
have neg : ∀ (h : ¬e.BoundaryGE i),
  Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j) (Iso.hom (XIso K e h) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry))
      (Iso.hom (XIso K e sorry) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)))
    0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have neg : Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
  (CategoryStruct.comp (Y := X K e j)
    (if hij : c.Rel i j then
      if hi : e.BoundaryGE i then Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
      else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e sorry)
    else 0)
    0)
  0
Tactic: rw [dif_neg hjk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
neg :
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      0)
    0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have neg₁ : Eq.{v_1 + 1} (α := X K e i ⟶ X K e k) 0 0
Tactic: rw [dif_neg hjk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : ¬c.Rel i j
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have neg : Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
  (CategoryStruct.comp (Y := X K e j) 0
    (if hij : c.Rel j k then
      if hi : e.BoundaryGE j then Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
      else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e sorry)
    else 0))
  0
Tactic: rw [dif_neg hij, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : ¬c.Rel i j
neg :
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j) 0
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
have neg₁ : Eq.{v_1 + 1} (α := X K e i ⟶ X K e k) 0 0
Tactic: rw [dif_neg hij, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ K.X (e.f i) = K.X i'
have subst : K.X (e.f i) = K.X (e.f i)
Tactic: subst hi'
Cleared hypotheses: i', hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ K.opcycles (e.f i) = K.opcycles i'
have subst : K.opcycles (e.f i) = K.opcycles (e.f i)
Tactic: subst hi'
Cleared hypotheses: i', hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : ¬e.BoundaryGE i
⊢ (K.truncGE' e).d i j = Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)
have dsimp : Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
  (if hij : c.Rel i j then
      if hi : e.BoundaryGE i then
        Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry)
      else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry)
    else 0 :
    truncGE'.X K e i ⟶ truncGE'.X K e j)
  (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' sorry) :
    truncGE'.X K e i ⟶ truncGE'.X K e j)
Tactic: dsimp [truncGE', truncGE'.d]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : ¬e.BoundaryGE i
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
        else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
      else 0 :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯) :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
have rw : Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
  (Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry))
  (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' sorry))
Tactic: rw [dif_pos hij, dif_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : ¬e.BoundaryGE i
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯))
have subst : Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
  (Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry))
  (Iso.hom (K.truncGE'XIso e sorry hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e sorry sorry))
Tactic: subst hi' hj'
Cleared hypotheses: i', j', hi', hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : e.BoundaryGE i
⊢ (K.truncGE' e).d i j =
    Iso.hom (K.truncGE'XIsoOpcycles e hi' hi) ≫ K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)
have dsimp : Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
  (if hij : c.Rel i j then
      if hi : e.BoundaryGE i then
        Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry)
      else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry)
    else 0 :
    truncGE'.X K e i ⟶ truncGE'.X K e j)
  (CategoryStruct.comp (Y := K.opcycles i') (Iso.hom (K.truncGE'XIsoOpcycles e hi' hi))
      (K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' sorry)) :
    truncGE'.X K e i ⟶ truncGE'.X K e j)
Tactic: dsimp [truncGE', truncGE'.d]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : e.BoundaryGE i
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
        else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
      else 0 :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
    (CategoryStruct.comp (Y := K.opcycles i') (Iso.hom (K.truncGE'XIsoOpcycles e hi' hi))
        (K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)) :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
have rw : Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
  (Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry))
  (CategoryStruct.comp (Y := K.opcycles i') (Iso.hom (K.truncGE'XIsoOpcycles e hi' hi))
    (K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' sorry)))
Tactic: rw [dif_pos hij, dif_pos hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : e.BoundaryGE i
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (CategoryStruct.comp (Y := K.opcycles i') (Iso.hom (K.truncGE'XIsoOpcycles e hi' hi))
      (K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)))
have subst : Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
  (Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e sorry))
  (CategoryStruct.comp (Y := K.opcycles (e.f i)) (Iso.hom (K.truncGE'XIsoOpcycles e sorry hi))
    (K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e sorry sorry)))
Tactic: subst hi' hj'
Cleared hypotheses: i', j', hi', hj'