awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
q n : ℤ
α : Cocycle K (Functor.obj (singleFunctor C q) X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
⊢ ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
have hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1))
  (δ n (n + 1) (↑((n + 1).negOnePow • α) : Cochain K ((singleFunctor C q).obj X) n)) 0
Tactic: have hα := ((n + 1).negOnePow • α).δ_eq_zero (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
q n : ℤ
α : Cocycle K (Functor.obj (singleFunctor C q) X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα :
  Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1))
    (δ n (n + 1) (↑((n + 1).negOnePow • α) : Cochain K ((singleFunctor C q).obj X) n)) 0
⊢ ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
have hα₁ : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) sorry) 0
Tactic: rw [coe_units_smul, δ_units_smul, ← hf, Cochain.δ_toSingleMk _ _ _ p' (by lia),
    smul_smul, Int.units_mul_self, one_smul] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
q n : ℤ
α : Cocycle K (Functor.obj (singleFunctor C q) X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
⊢ ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
have refine_1 : K.d p' p ≫ f = 0
Tactic: refine ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
q n : ℤ
α : Cocycle K (Functor.obj (singleFunctor C q) X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
refine_1 : K.d p' p ≫ f = 0
⊢ ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
have refine_2 : toSingleMk f h p' hp' sorry = α
Tactic: refine ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
q n : ℤ
α : Cocycle K (Functor.obj (singleFunctor C q) X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
⊢ toSingleMk f h p' hp' ⋯ = α
have refine_2 : (↑(toSingleMk f h p' hp' sorry) : Cochain K ((singleFunctor C q).obj X) n) = (↑α : Cochain K ((singleFunctor C q).obj X) n)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
⊢ Membership.mem (γ := AddSubgroup (Cocycle K (Functor.obj (singleFunctor C q) X) n))
      (coboundaries K (Functor.obj (singleFunctor C q) X) n) (toSingleMk f h p' hp' hf) ↔
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
have rw : (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
    δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) ↔
  ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
Tactic: rw [mem_coboundaries_iff _ (n - 1) (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
⊢ (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
      δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) ↔
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
have mp : (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
    δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) →
  ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
mp :
  (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
      δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) →
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
⊢ (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
      δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) ↔
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
have mpr : (∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f) →
  ∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
    δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
⊢ ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
have mp : ∀ (g : K.X p'' ⟶ X) (hg : Cochain.toSingleMk g sorry = α), ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
Tactic: obtain ⟨g, hg⟩ := Cochain.toSingleMk_surjective α p'' (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
g : K.X p'' ⟶ X
hg : Cochain.toSingleMk g ⋯ = α
⊢ ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
have mp : K.d p p'' ≫ (n.negOnePow • g) = f
Tactic: refine ⟨n.negOnePow • g, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
g : K.X p'' ⟶ X
hg : Cochain.toSingleMk g ⋯ = α
⊢ K.d p p'' ≫ (n.negOnePow • g) = f
have hα₁ : HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n) n.negOnePow (Cochain.toSingleMk (K.d p p'' ≫ g) h) =
  Cochain.toSingleMk f h
Tactic: rw [← hg, toSingleMk_coe, Cochain.δ_toSingleMk _ _ _ _ h] at hα
Cleared hypotheses: hα, hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
⊢ ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
    ShortComplex.Exact ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n))
have hT₁ : ∃ (S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)) (σ :
  (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
  Nonempty.{v_1 + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
Tactic: rw [distinguished_iff_iso_trianglehOfDegreewiseSplit] at hT
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT_1 :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
hT :
  ∃ (S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)) (σ :
    (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))),
    Nonempty.{v_1 + 1} (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
⊢ ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
    ShortComplex.Exact ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n))
have obtain : ∀ (S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ))
  (σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)))
  (e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ),
  ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
    ShortComplex.Exact ((Pretriangulated.shortComplexOfDistTriangle T' sorry).map (homologyFunctor C (ComplexShape.up ℤ) n))
Tactic: obtain ⟨S, σ, ⟨e⟩⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n))
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ ∃ (T' : Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))) (e : T ≅ T'),
    ShortComplex.Exact ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n))
have hS : S.ShortExact
Tactic: have hS := HomologicalComplex.shortExact_of_degreewise_shortExact S
      (fun n => (σ n).shortExact)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ L.IsKInjective ↔
    ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
have refine_1 : L.IsKInjective →
  ∀ (K : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
    (f : K ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (hK : HomotopyCategory.subcategoryAcyclic C K), f = 0
Tactic: refine ⟨fun _ K f hK ↦ ?_,
      fun hL ↦ ⟨fun {K} f hK ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
refine_1 :
  L.IsKInjective →
    ∀ (K : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
      (f : K ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
      (hK : HomotopyCategory.subcategoryAcyclic C K), f = 0
⊢ L.IsKInjective ↔
    ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
have refine_2 : ∀
  (hL :
    ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
  {K : CochainComplex.{v_1, u_1, 0} C ℤ} (f : K ⟶ L) (hK : HomologicalComplex.Acyclic K),
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
Tactic: refine ⟨fun _ K f hK ↦ ?_,
      fun hL ↦ ⟨fun {K} f hK ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
f : K ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L
hK : HomotopyCategory.subcategoryAcyclic C K
⊢ f = 0
have refine_1 : ∀ (K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ))
  (f :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  (hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)), f = 0
Tactic: obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
Cleared hypotheses: K, f, hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
f :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L
hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
⊢ f = 0
have refine_1 : ∀ (f : K ⟶ L),
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0
Tactic: obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
f : K ⟶ L
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0
have refine_1 : ∀ (hK : K.Acyclic) (f : K ⟶ L),
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0
Tactic: rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK
Cleared hypotheses: hK, f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hK : K.Acyclic
f : K ⟶ L
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0
have refine_1 : Eq.{v_1 + 1} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0) 0
Tactic: rw [HomotopyCategory.eq_of_homotopy f 0 (IsKInjective.homotopyZero f hK), Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : L.IsKInjective
K : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hK : K.Acyclic
f : K ⟶ L
refine_1 :
  Eq.{v_1 + 1} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0) 0
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f) 0
have refine_1₁ : Eq.{v_1 + 1} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  0 0
Tactic: rw [HomotopyCategory.eq_of_homotopy f 0 (IsKInjective.homotopyZero f hK), Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL :
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
have hK₁ : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
Tactic: rw [← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL :
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
have refine_2 : Eq.{max 1 (v_1 + 1)} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  0 (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
Tactic: rw [hL ((HomotopyCategory.quotient _ _).map f) hK, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL :
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
refine_2 :
  Eq.{max 1 (v_1 + 1)} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    0 (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
have refine_2₁ : Eq.{max 1 (v_1 + 1)} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  0 0
Tactic: rw [hL ((HomotopyCategory.quotient _ _).map f) hK, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
hL : L.IsKInjective
n : ℤ
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L).IsKInjective
have rw : ∀
  (hL :
    ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
  (n : ℤ),
  ObjectProperty.rightOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L))
Tactic: rw [isKInjective_iff_rightOrthogonal] at hL ⊢
Cleared hypotheses: hL, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n m : ℤ
hnm : n + 1 = m
hK : HomologicalComplex.ExactAt K m
inst_2 : Injective.{v_1, u_1} (L.X m)
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) m
have subst : ∀ (hK : HomologicalComplex.ExactAt K (n + 1)) [Injective.{v_1, u_1} (L.X (n + 1))],
  ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)
Tactic: subst hnm
Cleared hypotheses: m, hnm, hK, inst_2