awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
pos :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
pos₁ :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
pos₂ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₃ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₄ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ 0)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₅ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ (if k₀ = k₀ then 𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀) else 0) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
have pos₆ : Eq.{v_1 + 1} (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0
  (CategoryStruct.comp (Y := X (double f hi₀₁) k₁) 0
    (if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0))
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
pos :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
pos₁ :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
pos₂ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₃ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₄ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ 0)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₅ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₆ :
  Eq.{v_1 + 1} (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0
    (CategoryStruct.comp (Y := X (double f hi₀₁) k₁) 0
      (if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0))
⊢ (if k₀ = k₀ then 𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀) else 0) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
have pos₇ : Eq.{v_1 + 1} (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0 0
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ Eq (α := X (double f hi₀₁) i₀ ⟶ K.X i₀) (Hom.f (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ) i₀)
    (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀)
have dsimp : (if i₀ = i₀ then 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀)
  else if hk₁ : i₀ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0) =
  Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
Tactic: dsimp [mkHomFromDouble]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (if i₀ = i₀ then 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
have rw : 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀) = Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
Tactic: rw [if_pos rfl, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
rw : 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀) = Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
⊢ (if i₀ = i₀ then 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
have rw₁ : Eq (α := X (double f hi₀₁) i₀ ⟶ K.X i₀) (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀))
  (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀)
Tactic: rw [if_pos rfl, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
rw : 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀) = Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
rw₁ :
  Eq (α := X (double f hi₀₁) i₀ ⟶ K.X i₀) (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀))
    (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀)
⊢ (if i₀ = i₀ then 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
have rw₂ : Eq (α := X (double f hi₀₁) i₀ ⟶ K.X i₀) (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀) (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀)
Tactic: rw [if_pos rfl, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁) (Hom.f (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ) i₁)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
have dsimp : Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁)
  (if hk₀ : i₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
  else if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0)
  (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
Tactic: dsimp [mkHomFromDouble]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁)
    (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
have rw : (if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
  Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
Tactic: rw [dif_neg h.symm, if_pos rfl, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
rw :
  (if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
    Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
⊢ Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁)
    (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
have rw₁ : 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) = Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
Tactic: rw [dif_neg h.symm, if_pos rfl, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
rw :
  (if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
    Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
rw₁ : 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) = Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
⊢ Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁)
    (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
have rw₂ : Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁))
  (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
Tactic: rw [dif_neg h.symm, if_pos rfl, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
rw :
  (if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
    Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
rw₁ : 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) = Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
rw₂ :
  Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁))
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
⊢ Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁)
    (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
have rw₃ : Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
Tactic: rw [dif_neg h.symm, if_pos rfl, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
g : double (𝟙 X) hi₀₁ ⟶ K
⊢ (fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
        (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
      ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g) =
    g
have h₀ : Hom.f
    ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
        (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) sorry sorry : double (𝟙 X) hi₀₁ ⟶ K))
      ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g))
    i₀ =
  g.f i₀
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
g : double (𝟙 X) hi₀₁ ⟶ K
h₀ :
  Hom.f
      ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
          (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
        ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g))
      i₀ =
    g.f i₀
⊢ (fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
        (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
      ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g) =
    g
have h₁ : Hom.f
    ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
        (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) sorry sorry : double (𝟙 X) hi₀₁ ⟶ K))
      ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g))
    i₁ =
  g.f i₁
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (if hj : ∃ (k : ι), c.Rel j k then double (𝟙 X) ⋯ else Functor.obj (single C c j) X)
have pos : (h : ∃ (k : ι), c.Rel j k) →
  Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (double (𝟙 X) sorry)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
pos :
  (h : ∃ (k : ι), c.Rel j k) →
    Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
      (double (𝟙 X) ⋯)
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (if hj : ∃ (k : ι), c.Rel j k then double (𝟙 X) ⋯ else Functor.obj (single C c j) X)
have neg : (h : ¬∃ (k : ι), c.Rel j k) →
  Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (Functor.obj (single C c j) X)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (Functor.obj (single C c j) X)
have neg : ∀ (j_1 : ι), ¬c.Rel j j_1
Tactic: apply evalCompCoyonedaCorepresentableBySingle
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1
have neg : (∃ (k : ι), c.Rel j k ∧ j ≠ k) → ∀ (j_1 : ι), ¬c.Rel j j_1
Tactic: obtain _ | _ := c.exists_distinct_prev_or j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
neg : (∃ (k : ι), c.Rel j k ∧ j ≠ k) → ∀ (j_1 : ι), ¬c.Rel j j_1
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1
have neg₁ : (∀ (k : ι), ¬c.Rel j k) → ∀ (j_1 : ι), ¬c.Rel j j_1
Tactic: obtain _ | _ := c.exists_distinct_prev_or j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
h_1 : ∃ (k : ι), c.Rel j k ∧ j ≠ k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1
have neg : ∀ (j_1 w : ι), c.Rel j w → j ≠ w → ¬c.Rel j j_1
Tactic: tauto
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (if hj : ∃ (k : ι), c.Rel j k then double (𝟙 X) ⋯ else Functor.obj (single C c j) X)
have pos : (h : ∃ (k : ι), c.Rel j k) →
  Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (double (𝟙 X) sorry)
Tactic: classical
  split_ifs with h
  · exact evalCompCoyonedaCorepresentableByDoubleId _
      (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _
  · apply evalCompCoyonedaCorepresentableBySingle
    obtain _ | _ := c.exists_distinct_prev_or j <;> tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
pos :
  (h : ∃ (k : ι), c.Rel j k) →
    Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
      (double (𝟙 X) ⋯)
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (if hj : ∃ (k : ι), c.Rel j k then double (𝟙 X) ⋯ else Functor.obj (single C c j) X)
have neg : (h : ¬∃ (k : ι), c.Rel j k) →
  Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (Functor.obj (single C c j) X)
Tactic: classical
  split_ifs with h
  · exact evalCompCoyonedaCorepresentableByDoubleId _
      (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _
  · apply evalCompCoyonedaCorepresentableBySingle
    obtain _ | _ := c.exists_distinct_prev_or j <;> tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i : ι
hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ i
⊢ ∃ (i₁ : ι₁), i = e₁.f i₁
have inl : ∀ (i₁ : ι₁) (hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ e₁.f i₁), ∃ (i₁_1 : ι₁), e₁.f i₁ = e₁.f i₁_1
Tactic: obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i : ι
hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ i
inl : ∀ (i₁ : ι₁) (hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ e₁.f i₁), ∃ (i₁_1 : ι₁), e₁.f i₁ = e₁.f i₁_1
⊢ ∃ (i₁ : ι₁), i = e₁.f i₁
have inr : ∀ (i₂ : ι₂) (hi : ∀ (i₂_1 : ι₂), e₂.f i₂_1 ≠ e₂.f i₂), ∃ (i₁ : ι₁), e₂.f i₂ = e₁.f i₁
Tactic: obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
hi : ∀ (i₂_1 : ι₂), e₂.f i₂_1 ≠ e₂.f i₂
⊢ ∃ (i₁ : ι₁), e₂.f i₂ = e₁.f i₁
have inr : False
Tactic: exfalso