awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₂ : K.d i' (e.f j) ≫ Iso.hom (Iso.refl ((K.restriction e).X j)) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₃ : K.d i' (e.f j) ≫ 𝟙 ((K.restriction e).X j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₄ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e sorry)) 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₂ : K.d i' (e.f j) ≫ Iso.hom (Iso.refl ((K.restriction e).X j)) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₃ : K.d i' (e.f j) ≫ 𝟙 ((K.restriction e).X j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₄ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₅ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ (L.extend e).d i' (e.f j) ≫ Iso.hom (L.extendXIso e sorry)) 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₂ : K.d i' (e.f j) ≫ Iso.hom (Iso.refl ((K.restriction e).X j)) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₃ : K.d i' (e.f j) ≫ 𝟙 ((K.restriction e).X j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₄ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₅ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ (L.extend e).d i' (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₆ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ CategoryStruct.comp (Y := (L.extend e).X (e.f j)) 0 (Iso.hom (L.extendXIso e sorry))) 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₂ : K.d i' (e.f j) ≫ Iso.hom (Iso.refl ((K.restriction e).X j)) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₃ : K.d i' (e.f j) ≫ 𝟙 ((K.restriction e).X j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₄ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₅ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ (L.extend e).d i' (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₆ :
  Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ CategoryStruct.comp (Y := (L.extend e).X (e.f j)) 0 (Iso.hom (L.extendXIso e ⋯))) 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₇ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ 0) 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₂ : K.d i' (e.f j) ≫ Iso.hom (Iso.refl ((K.restriction e).X j)) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₃ : K.d i' (e.f j) ≫ 𝟙 ((K.restriction e).X j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₄ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₅ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ (L.extend e).d i' (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₆ :
  Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ CategoryStruct.comp (Y := (L.extend e).X (e.f j)) 0 (Iso.hom (L.extendXIso e ⋯))) 0
rw₇ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ 0) 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₈ : Eq.{v_1 + 1} (α := K.X i' ⟶ L.X j) 0 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
⊢ e.liftExtend (e.homRestrict ψ) ⋯ = ψ
have h : ∀ (i' : ι'), Hom.f (e.liftExtend (e.homRestrict ψ) sorry) i' = ψ.f i'
Tactic: ext i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
⊢ Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Hom.f (e.liftExtend (e.homRestrict ψ) sorry) i' = ψ.f i'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'
⊢ Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), Hom.f (e.liftExtend (e.homRestrict ψ) sorry) i' = ψ.f i'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'
have pos : ∀ (i : ι),
  Eq (α := K.X (e.f i) ⟶ (L.extend e).X (e.f i)) (Hom.f (e.liftExtend (e.homRestrict ψ) sorry) (e.f i)) (ψ.f (e.f i))
Tactic: obtain ⟨i, rfl⟩ := hi'
Cleared hypotheses: i', hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
⊢ e.homRestrict (e.liftExtend φ hφ) = φ
have h : ∀ (i : ι), Hom.f (e.homRestrict (e.liftExtend φ hφ)) i = φ.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K K' : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
α : K' ⟶ K
ψ : K ⟶ L.extend e
⊢ Eq (α := K'.restriction e ⟶ L) (e.homRestrict (α ≫ ψ)) (restrictionMap α e ≫ e.homRestrict ψ)
have h : ∀ (i : ι),
  Eq (α := (K'.restriction e).X i ⟶ L.X i) (Hom.f (e.homRestrict (α ≫ ψ)) i)
    (Hom.f (restrictionMap α e ≫ e.homRestrict ψ) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L L' : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
⊢ Eq (α := K.restriction e ⟶ L') (e.homRestrict (ψ ≫ extendMap β e)) (e.homRestrict ψ ≫ β)
have h : ∀ (i : ι),
  Eq (α := (K.restriction e).X i ⟶ L'.X i) (Hom.f (e.homRestrict (ψ ≫ extendMap β e)) i) (Hom.f (e.homRestrict ψ ≫ β) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
⊢ IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
have mp : IsZero K → K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
mp : IsZero K → K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
⊢ IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
have mpr : K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e → IsZero K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
hK : IsZero K
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
have mp : K.IsStrictlySupported e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
hK : IsZero K
mp : K.IsStrictlySupported e
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
have mp₁ : K.IsStrictlySupportedOutside e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
hK : IsZero K
⊢ K.IsStrictlySupported e
have mp : ∀ (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i'), IsZero.{v_1, u_3} (K.X i')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
hK : IsZero K
⊢ K.IsStrictlySupportedOutside e
have mp : ∀ (i : ι), IsZero.{v_1, u_3} (K.X (e.f i))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
⊢ IsZero K
have mpr : Eq (α := K ⟶ K) (𝟙 K) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
⊢ Eq (α := K ⟶ K) (𝟙 K) 0
have mpr : ∀ (n : ι'), Hom.f (𝟙 K) n = Hom.f 0 n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ Hom.f (𝟙 K) n = Hom.f 0 n
have mpr : IsZero.{v_1, u_3} (K.X n)
Tactic: apply IsZero.eq_of_src
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ IsZero.{v_1, u_3} (K.X n)
have pos : ∀ (hn : ∃ (i : ι), e.f i = n), IsZero.{v_1, u_3} (K.X n)
Tactic: by_cases hn : ∃ i, e.f i = n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
pos : ∀ (hn : ∃ (i : ι), e.f i = n), IsZero.{v_1, u_3} (K.X n)
⊢ IsZero.{v_1, u_3} (K.X n)
have neg : ∀ (hn : ¬∃ (i : ι), e.f i = n), IsZero.{v_1, u_3} (K.X n)
Tactic: by_cases hn : ∃ i, e.f i = n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ∃ (i : ι), e.f i = n
⊢ IsZero.{v_1, u_3} (K.X n)
have pos : ∀ (i : ι), IsZero.{v_1, u_3} (K.X (e.f i))
Tactic: obtain ⟨i, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero.{v_2, u_4} (X (Functor.obj (F.mapHomologicalComplex c') K) i')
have rw : Eq.{v_2 + 1} (α :=
  X (Functor.obj (F.mapHomologicalComplex c') K) i' ⟶ X (Functor.obj (F.mapHomologicalComplex c') K) i')
  (𝟙 (X (Functor.obj (F.mapHomologicalComplex c') K) i')) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Eq.{v_2 + 1} (α :=
    X (Functor.obj (F.mapHomologicalComplex c') K) i' ⟶ X (Functor.obj (F.mapHomologicalComplex c') K) i')
    (𝟙 (X (Functor.obj (F.mapHomologicalComplex c') K) i')) 0
have dsimp : Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (𝟙 (F.obj (K.X i'))) 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (𝟙 (F.obj (K.X i'))) 0
have rw : F.map (𝟙 (K.X i')) = 0
Tactic: rw [← F.map_id, (K.isZero_X_of_isStrictlySupported e i' hi').eq_of_src (𝟙 _) 0, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
rw : F.map (𝟙 (K.X i')) = 0
⊢ Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (𝟙 (F.obj (K.X i'))) 0
have rw₁ : Eq (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (F.map 0) 0
Tactic: rw [← F.map_id, (K.isZero_X_of_isStrictlySupported e i' hi').eq_of_src (𝟙 _) 0, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.IsSupported (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
rw : F.map (𝟙 (K.X i')) = 0
rw₁ : Eq (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (F.map 0) 0
⊢ Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (𝟙 (F.obj (K.X i'))) 0
have rw₂ : Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) 0 0
Tactic: rw [← F.map_id, (K.isZero_X_of_isStrictlySupported e i' hi').eq_of_src (𝟙 _) 0, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Restriction (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.IsRelIff
i j : ι
i' j' : ι'
hi : e.f i = i'
hj : e.f j = j'
⊢ (K.restriction e).d i j = Iso.hom (K.restrictionXIso e hi) ≫ K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj)
have subst : (K.restriction e).d i j = Iso.hom (K.restrictionXIso e sorry) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.restrictionXIso e sorry)
Tactic: subst hi hj
Cleared hypotheses: i', j', hi, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Restriction (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.IsRelIff
i : ι
i' : ι'
hi : e.f i = i'
⊢ Eq (α := (K.restriction e).X i ⟶ (L.restriction e).X i) (Hom.f (restrictionMap φ e) i)
    (Iso.hom (K.restrictionXIso e hi) ≫ φ.f i' ≫ Iso.inv (L.restrictionXIso e hi))
have subst : Eq (α := (K.restriction e).X i ⟶ (L.restriction e).X i) (Hom.f (restrictionMap φ e) i)
  (Iso.hom (K.restrictionXIso e sorry) ≫ φ.f (e.f i) ≫ Iso.inv (L.restrictionXIso e sorry))
Tactic: subst hi
Cleared hypotheses: i', hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
⊢ Iso.hom (K.restrictionXIso e hi') ≫ (K.sc' i' j' k').f =
    ((K.restriction e).sc' i j k).f ≫ Iso.hom (K.restrictionXIso e hj')
have subst : ∀ (hk'' : c'.next (e.f j) = k') (hi'' : c'.prev (e.f j) = e.f i),
  Iso.hom (K.restrictionXIso e sorry) ≫ (K.sc' (e.f i) (e.f j) k').f =
    ((K.restriction e).sc' i j k).f ≫ Iso.hom (K.restrictionXIso e sorry)
Tactic: subst hi' hj'
Cleared hypotheses: i', j', hi', hj', hi'', hk''