awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have pos : ∀ (hjk : c.Rel j k), (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
pos : ∀ (hjk : c.Rel j k), (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have neg : ∀ (hjk : ¬c.Rel j k), (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have pos : Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
  (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
    (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e sorry sorry)))
  0
Tactic: rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
    homologyι_comp_fromOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
pos :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
      (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have pos₁ : Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
  (K.homologyι j' ≫
    CategoryStruct.comp (Y := (K.truncGE' e).X j) (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
      (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e sorry sorry)))
  0
Tactic: rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
    homologyι_comp_fromOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
pos :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
      (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
pos₁ :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (K.homologyι j' ≫
      CategoryStruct.comp (Y := (K.truncGE' e).X j) (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
        (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have pos₂ : Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
  (K.homologyι j' ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e sorry sorry)) 0
Tactic: rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
    homologyι_comp_fromOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
pos :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
      (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
pos₁ :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (K.homologyι j' ≫
      CategoryStruct.comp (Y := (K.truncGE' e).X j) (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
        (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
pos₂ :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (K.homologyι j' ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)) 0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have pos₃ : Eq (α := K.homology j' ⟶ (K.truncGE' e).X k) (0 ≫ Iso.inv (K.truncGE'XIso e sorry sorry)) 0
Tactic: rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
    homologyι_comp_fromOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
pos :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
      (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
pos₁ :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (K.homologyι j' ≫
      CategoryStruct.comp (Y := (K.truncGE' e).X j) (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
        (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
pos₂ :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (K.homologyι j' ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)) 0
pos₃ : Eq (α := K.homology j' ⟶ (K.truncGE' e).X k) (0 ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)) 0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have pos₄ : Eq.{v_1 + 1} (α := K.homology j' ⟶ (K.truncGE' e).X k) 0 0
Tactic: rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
    homologyι_comp_fromOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have neg : Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
  (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) 0) 0
Tactic: rw [shape _ _ _ hjk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
neg :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) 0) 0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
have neg₁ : Eq.{v_1 + 1} (α := K.homology j' ⟶ (K.truncGE' e).X k) 0 0
Tactic: rw [shape _ _ _ hjk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (hypothesis)
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 j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)
have hk' : c'.next j' = e.f k
Tactic: have hk' : c'.next j' = e.f k := by simpa only [hj'] using e.next_f hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
⊢ IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)
have pos : (hjk : c.Rel j k) →
  IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) sorry)
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
pos :
  (hjk : c.Rel j k) →
    IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
      (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)
⊢ IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)
have neg : (hjk : ¬c.Rel j k) →
  IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) sorry)
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (hypothesis)
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 j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : ¬c.Rel j k
⊢ IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)
have this : IsIso (X := K.homology j') (K.homologyι j')
Tactic: have := K.isIso_homologyι _ _ hk'
      (shape _ _ _ (by simpa only [← hj', e.rel_iff] using hjk))
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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_1 j k : ι
hi : c.prev j = i_1
hk : c.next j = k
i : ι
⊢ (K.truncGE' e).HasHomology i
have pos : ∀ (hi : e.BoundaryGE i), (K.truncGE' e).HasHomology i
Tactic: by_cases hi : e.BoundaryGE i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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_1 j k : ι
hi : c.prev j = i_1
hk : c.next j = k
i : ι
pos : ∀ (hi : e.BoundaryGE i), (K.truncGE' e).HasHomology i
⊢ (K.truncGE' e).HasHomology i
have neg : ∀ (hi : ¬e.BoundaryGE i), (K.truncGE' e).HasHomology i
Tactic: by_cases hi : e.BoundaryGE i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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'
inst_5 : HasZeroObject.{v_1, u_3} C
i' : ι'
⊢ (K.truncGE e).HasHomology i'
have dsimp : ((K.truncGE' e).extend e).HasHomology i'
Tactic: dsimp [truncGE]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
⊢ e.f k = c'.next j'
have rw : e.f k = c'.next (e.f j)
Tactic: rw [← hj', e.next_f hk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
rw : e.f k = c'.next (e.f j)
⊢ e.f k = c'.next j'
have rw₁ : e.f k = e.f k
Tactic: rw [← hj', e.next_f hk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (hypothesis)
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'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
⊢ Eq (α :=
    (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
      (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
    (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
        (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) : K.opcycles j' ⟶ (K.truncGE' e).X j)
        (ShortComplex.RightHomologyData.g'
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))) :
      (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
        (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
    ((ShortComplex.RightHomologyData.canonical (K.sc j')).g' ≫
        ShortComplex.Hom.τ₃ (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)) :
      (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
        (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
have hk' : e.f k = c'.next j'
Tactic: have hk' : e.f k = c'.next j' := by rw [← hj', e.next_f hk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
⊢ Eq (α :=
    (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
      (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
    (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
        (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) : K.opcycles j' ⟶ (K.truncGE' e).X j)
        (ShortComplex.RightHomologyData.g'
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))) :
      (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
        (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
    ((ShortComplex.RightHomologyData.canonical (K.sc j')).g' ≫
        ShortComplex.Hom.τ₃ (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)) :
      (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
        (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
have dsimp : Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
  (CategoryStruct.comp (Y :=
      ShortComplex.RightHomologyData.Q (S := (K.truncGE' e).sc' i j k)
        (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))
      (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) : K.opcycles j' ⟶ (K.truncGE' e).X j)
      (ShortComplex.RightHomologyData.g'
        (extend.rightHomologyData (K.truncGE' e) e hj' hi sorry hk sorry
          (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))) :
    (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
  ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫ Hom.f (K.πTruncGE e) (c'.next j') :
    (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := (K.truncGE' e).sc' i j k)
          (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))
        (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) : K.opcycles j' ⟶ (K.truncGE' e).X j)
        (ShortComplex.RightHomologyData.g'
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))) :
      (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫ Hom.f (K.πTruncGE e) (c'.next j') :
      (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
have rw : Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
  (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
  ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
    Iso.inv (K.restrictionXIso e hk') ≫ Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: rw [extend.rightHomologyData_g' _ _ _ _ _ _ _ _ hk', πTruncGE,
        e.liftExtend_f _ _ hk', truncGE'.homologyData_right_g']
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have pos : ∀ (hjk : c.Rel j k),
  Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: by_cases hjk : c.Rel j k