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 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 j : ι
hij : c.Rel i j
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫
      if hi : e.BoundaryGE j then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f j) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)
have rw : (if hi : e.BoundaryGE i then
      Iso.hom (K.truncGE'XIsoOpcycles e sorry hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e sorry hi)
    else Iso.hom (K.truncGE'XIso e sorry hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e sorry hi)) ≫
    (L.truncGE' e).d i j =
  (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e sorry sorry) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e sorry sorry)
Tactic: rw [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 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 j : ι
hij : c.Rel i j
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
have pos : ∀ (hi : e.BoundaryGE i),
  (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e sorry hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e sorry hi)
      else Iso.hom (K.truncGE'XIso e sorry hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e sorry hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e sorry sorry) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e sorry sorry)
Tactic: by_cases hi : e.BoundaryGE i
-- 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 j : ι
hij : c.Rel i j
pos :
  ∀ (hi : e.BoundaryGE i),
    (if hi : e.BoundaryGE i then
          Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
        else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
        (L.truncGE' e).d i j =
      (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
have neg : ∀ (hi : ¬e.BoundaryGE i),
  (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e sorry hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e sorry hi)
      else Iso.hom (K.truncGE'XIso e sorry hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e sorry hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e sorry sorry) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e sorry sorry)
Tactic: by_cases hi : e.BoundaryGE i
-- 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 j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
have pos : (Iso.hom (K.truncGE'XIsoOpcycles e sorry hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e sorry hi)) ≫
    (L.truncGE' e).d i j =
  (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e sorry sorry) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e sorry sorry)
Tactic: rw [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 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 j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
have neg : (Iso.hom (K.truncGE'XIso e sorry hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e sorry hi)) ≫ (L.truncGE' e).d i j =
  (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e sorry sorry) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e sorry sorry)
Tactic: rw [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 L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryGE i
i' : ι'
h : e.f i = i'
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIsoOpcycles e h hi) ≫ opcyclesMap φ i' ≫ Iso.inv (L.truncGE'XIsoOpcycles e h hi))
have subst : Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
  (Iso.hom (K.truncGE'XIsoOpcycles e sorry hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e sorry hi))
Tactic: subst h
Cleared hypotheses: i', h
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
i' : ι'
h : e.f i = i'
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIso e h hi) ≫ φ.f i' ≫ Iso.inv (L.truncGE'XIso e h hi))
have subst : Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
  (Iso.hom (K.truncGE'XIso e sorry hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e sorry hi))
Tactic: subst h
Cleared hypotheses: i', h
-- 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'
⊢ truncGE'Map (𝟙 K) e = 𝟙 (K.truncGE' e)
have h : ∀ (i : ι), Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
Tactic: ext i
-- 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 : ι
⊢ Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
have pos : ∀ (hi : e.BoundaryGE i), Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
Tactic: by_cases hi : e.BoundaryGE i
-- 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 : ι
pos : ∀ (hi : e.BoundaryGE i), Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
⊢ Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
have neg : ∀ (hi : ¬e.BoundaryGE i), Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
Tactic: by_cases hi : e.BoundaryGE i
-- 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'
⊢ Eq (α := K.truncGE' e ⟶ M.truncGE' e) (truncGE'Map (φ ≫ φ') e)
    (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e))
have h : ∀ (i : ι),
  Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
Tactic: ext i
-- 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 : ι
⊢ Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
have pos : ∀ (hi : e.BoundaryGE i),
  Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
Tactic: by_cases hi : e.BoundaryGE i
-- 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 : ι
pos :
  ∀ (hi : e.BoundaryGE i),
    Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
      (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
⊢ Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
have neg : ∀ (hi : ¬e.BoundaryGE i),
  Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
Tactic: by_cases hi : e.BoundaryGE i
-- 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 : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X i) (f K e i)
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi))
have dsimp : Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i)
  (if hi : e.BoundaryGE i then K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e sorry hi)
    else Iso.inv (K.truncGE'XIso e sorry hi) :
    K.X (e.f i) ⟶ (K.truncGE' e).X i)
  (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi) :
    K.X (e.f i) ⟶ (K.truncGE' e).X i)
Tactic: dsimp [f]
-- 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 : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (if hi : e.BoundaryGE i then K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.inv (K.truncGE'XIso e ⋯ hi) :
      K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi) :
      K.X (e.f i) ⟶ (K.truncGE' e).X i)
have rw : Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e sorry hi))
  (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi))
Tactic: rw [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 : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi))
have subst : Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e sorry hi))
  (Iso.hom (K.restrictionXIso e sorry) ≫ K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e sorry hi))
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 : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X i) (f K e i)
    (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso e hi' hi))
have dsimp : Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i)
  (if hi : e.BoundaryGE i then K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e sorry hi)
    else Iso.inv (K.truncGE'XIso e sorry hi) :
    K.X (e.f i) ⟶ (K.truncGE' e).X i)
  (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso e hi' hi) : K.X (e.f i) ⟶ (K.truncGE' e).X i)
Tactic: dsimp [f]
-- 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 : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (if hi : e.BoundaryGE i then K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.inv (K.truncGE'XIso e ⋯ hi) :
      K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso e hi' hi) : K.X (e.f i) ⟶ (K.truncGE' e).X i)
have rw : Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (Iso.inv (K.truncGE'XIso e sorry hi))
  (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso e hi' hi))
Tactic: rw [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 : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (Iso.inv (K.truncGE'XIso e ⋯ hi))
    (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso e hi' hi))
have subst : Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (Iso.inv (K.truncGE'XIso e sorry hi))
  (Iso.hom (K.restrictionXIso e sorry) ≫ Iso.inv (K.truncGE'XIso e sorry hi))
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 : ι
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
have pos : ∀ (hij : c.Rel i j), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
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 : ι
pos : ∀ (hij : c.Rel i j), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
have neg : ∀ (hij : ¬c.Rel i j), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
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 : ι
hij : c.Rel i j
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
have pos : ∀ (hi : e.BoundaryGE i), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
Tactic: by_cases hi : e.BoundaryGE i
-- 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
pos : ∀ (hi : e.BoundaryGE i), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
have neg : ∀ (hi : ¬e.BoundaryGE i), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
Tactic: by_cases hi : e.BoundaryGE i
-- 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
hi : e.BoundaryGE i
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
have pos : Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X j)
  (CategoryStruct.comp (Y := (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e sorry) ≫ K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e sorry hi))
    (Iso.hom (K.truncGE'XIsoOpcycles e sorry hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e sorry sorry)))
  ((K.restriction e).d i j ≫ Iso.hom (K.restrictionXIso e sorry) ≫ Iso.inv (K.truncGE'XIso e sorry sorry))
Tactic: rw [f_eq_iso_hom_pOpcycles_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq_fromOpcycles e hij rfl rfl 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
hi : ¬e.BoundaryGE i
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
have neg : Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X j)
  (CategoryStruct.comp (Y := (K.truncGE' e).X i) (Iso.hom (K.restrictionXIso e sorry) ≫ Iso.inv (K.truncGE'XIso e sorry hi))
    (Iso.hom (K.truncGE'XIso e sorry hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e sorry sorry)))
  ((K.restriction e).d i j ≫ Iso.hom (K.restrictionXIso e sorry) ≫ Iso.inv (K.truncGE'XIso e sorry sorry))
Tactic: rw [f_eq_iso_hom_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq e hij rfl rfl 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'
j : ι
hj : e.BoundaryGE j
i' : ι'
h : c'.Rel i' (e.f j)
⊢ Eq (α := K.X i' ⟶ (K.truncGE' e).X j) (K.d i' (e.f j) ≫ Hom.f (K.restrictionToTruncGE' e) j) 0
have dsimp : Eq (α := K.X i' ⟶ (K.truncGE' e).X j) (K.d i' (e.f j) ≫ restrictionToTruncGE'.f K e j) 0
Tactic: dsimp [restrictionToTruncGE']