awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasProduct.{v, v₁, u₁} c
inst_2 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ piObj.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
⊢ (f ≫ Pi.lift fun (b : β) ↦ factorThru (g ≫ Pi.π c b) f) = g
have h : ∀ (b : β),
  CategoryStruct.comp (Y := piObj.{v, v₁, u₁} c) (f ≫ Pi.lift fun (b : β) ↦ factorThru (g ≫ Pi.π c b) f) (Pi.π c b) =
    g ≫ Pi.π c b
Tactic: ext b
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ biprod.{v₁, u₁} P Q), f ≫ h = g
have refine : f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f) = g
Tactic: refine ⟨biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f) = g
have h₀ : CategoryStruct.comp (Y := biprod.{v₁, u₁} P Q)
    (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) biprod.fst =
  g ≫ biprod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBinaryBiproduct.{v₁, u₁} P Q
inst_3 : Injective.{v₁, u₁} P
inst_4 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ biprod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
h₀ :
  CategoryStruct.comp (Y := biprod.{v₁, u₁} P Q)
      (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) biprod.fst =
    g ≫ biprod.fst
⊢ f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f) = g
have h₁ : CategoryStruct.comp (Y := biprod.{v₁, u₁} P Q)
    (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) biprod.snd =
  g ≫ biprod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBiproduct.{v, v₁, u₁} c
inst_3 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ biproduct.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ biproduct.{v, v₁, u₁} c), f ≫ h = g
have refine : (f ≫ biproduct.lift fun (b : β) ↦ factorThru (g ≫ biproduct.π c b) f) = g
Tactic: refine ⟨biproduct.lift fun b => factorThru (g ≫ biproduct.π _ _) f, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasBiproduct.{v, v₁, u₁} c
inst_3 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ biproduct.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
⊢ (f ≫ biproduct.lift fun (b : β) ↦ factorThru (g ≫ biproduct.π c b) f) = g
have w : ∀ (j : β),
  CategoryStruct.comp (Y := biproduct.{v, v₁, u₁} c)
      (f ≫ biproduct.lift fun (b : β) ↦ factorThru (g ≫ biproduct.π c b) f) (biproduct.π c j) =
    g ≫ biproduct.π c j
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : C
⊢ Injective.{v₁, u₁} J ↔ Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda J)
have rw : Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op (op J))) ↔
  Functor.PreservesEpimorphisms.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda J)
Tactic: rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
⊢ ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
have pos : ∀ (h : IsZero.{v₁, u₁} X), ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
Tactic: by_cases h : IsZero X
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
pos : ∀ (h : IsZero.{v₁, u₁} X), ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
⊢ ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
have neg : ∀ (h : ¬IsZero.{v₁, u₁} X), ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
Tactic: by_cases h : IsZero X
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : EnoughInjectives.{v₁, u₁} C
X : C
h : IsZero.{v₁, u₁} X
⊢ ∃ (p : InjectivePresentation.{v₁, u₁} X), IsZero.{v₁, u₁} X → IsZero.{v₁, u₁} p.J
have this : Injective.{v₁, u₁} X
Tactic: have := h.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
I : D
hI : Injective.{v_1, u_1} I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst_3 : Mono g
⊢ ∃ (h : Y ⟶ G.obj I), g ≫ h = f
have rcases : ∀ (w : F.obj Y ⟶ I) (h : F.map g ≫ w = F.map f ≫ adj.counit.app I), ∃ (h : Y ⟶ G.obj I), g ≫ h = f
Tactic: rcases hI.factors (F.map f ≫ adj.counit.app _) (F.map g) with ⟨w,h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
I : D
hI : Injective.{v_1, u_1} I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst_3 : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ ∃ (h : Y ⟶ G.obj I), g ≫ h = f
have h₁ : g ≫ adj.unit.app Y ≫ G.map w = f
Tactic: use adj.unit.app Y ≫ G.map w
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
I : D
hI : Injective.{v_1, u_1} I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst_3 : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ g ≫ adj.unit.app Y ≫ G.map w = f
have h₁ : adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app I) = f
Tactic: rw [← unit_naturality_assoc, ← G.map_comp, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
⊢ ∃ (h : Y ⟶ I), g ≫ h = f
have this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
Tactic: haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
⊢ ∃ (h : Y ⟶ I), g ≫ h = f
have rcases : ∀ (w : G.obj Y ⟶ G.obj I) (h : G.map g ≫ w = G.map f), ∃ (h : Y ⟶ I), g ≫ h = f
Tactic: rcases hI.factors (G.map f) (G.map g) with ⟨w,h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
I : D
hI : Injective.{v₁, u₁} (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst_4 : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ ∃ (h : Y ⟶ I), g ≫ h = f
have h₁ : g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I = f
Tactic: use inv (adj.counit.app _) ≫ F.map w ≫ adj.counit.app _
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
G : Functor.{v_1, v₁, u_1, u₁} D C
adj : F ⊣ G
inst_2 : F.PreservesMonomorphisms
X : D
I : InjectivePresentation.{v_1, u_1} X
⊢ Mono (G.map I.f)
have this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
Tactic: haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesMonomorphisms
I : C
hI : Injective.{v_1, u_1} (F.obj I)
X Y : C
g : X ⟶ I
f : X ⟶ Y
h : Mono f
⊢ ∃ (h : Y ⟶ I), f ≫ h = g
have obtain : ∀ (h : F.obj Y ⟶ F.obj I) (fac : F.map f ≫ h = F.map g), ∃ (h : Y ⟶ I), f ≫ h = g
Tactic: obtain ⟨h, fac⟩ := hI.factors (F.map g) (F.map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
⊢ Injective.{v₁, u₁} X
have refine : ∀ {A B : C} (f : A ⟶ X) (e : A ⟶ B), Mono e → ∃ (h : B ⟶ X), e ≫ h = f
Tactic: refine Injective.mk (fun {A B} f e _ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
A B : C
f : A ⟶ X
e : A ⟶ B
h_1 : Mono e
⊢ ∃ (h : B ⟶ X), e ≫ h = f
have rcases : ∀ (g : B ⟶ Y) (hg : e ≫ g = f ≫ h.i), ∃ (h : B ⟶ X), e ≫ h = f
Tactic: rcases i.factors (f ≫ h.i) e with ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective.{v₁, u₁} Y
A B : C
f : A ⟶ X
e : A ⟶ B
h_1 : Mono e
g : B ⟶ Y
hg : e ≫ g = f ≫ h.i
⊢ ∃ (h : B ⟶ X), e ≫ h = f
have h₁ : e ≫ g ≫ h.r = f
Tactic: use g ≫ h.r
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
p : I ⟶ Z
hZ : IsZero.{v, u} Z
⊢ Injective.{v, u} I ↔ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
have obtain : Injective.{v, u} I ↔ MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
Tactic: obtain rfl := hZ.eq_of_tgt p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
⊢ Injective.{v, u} I ↔ MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
have mp : Injective.{v, u} I → MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
mp : Injective.{v, u} I → MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
⊢ Injective.{v, u} I ↔ MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
have mpr : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0 → Injective.{v, u} I
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : Injective.{v, u} I
A B : C
i : A ⟶ B
⊢ MorphismProperty.monomorphisms C i → HasLiftingProperty (X := I) (Y := Z) i 0
have mp : Mono i → HasLiftingProperty (X := I) (Y := Z) i 0
Tactic: (_ : Mono i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
⊢ Injective.{v, u} I
have mpr : ∀ {X Y : C} (g : X ⟶ I) (f : X ⟶ Y) [Mono f], ∃ (h : Y ⟶ I), f ≫ h = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
⊢ ∃ (h : B ⟶ I), i ≫ h = f
have this : HasLiftingProperty (X := I) (Y := Z) i 0
Tactic: have := h _ hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
I Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.rlp.{v, u} (MorphismProperty.monomorphisms C) (X := I) (Y := Z) 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty (X := I) (Y := Z) i 0
⊢ ∃ (h : B ⟶ I), i ≫ h = f
have sq : CommSq (Z := Z) f i 0 0
Tactic: have sq : CommSq f i (0 : I ⟶ Z) 0 := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Preserves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughInjectives.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
h : Mono f
⊢ Mono (F.map f)
have suffices : ∃ (h : F.obj Y ⟶ Injective.under.{v₂, u₂} (F.obj X)), F.map f ≫ h = Injective.ι (F.obj X)
Tactic: suffices ∃ h, F.map f ≫ h = Injective.ι (F.obj X) from mono_of_mono_fac this.choose_spec
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ ExactAt I.cocomplex (n + 1)
have rw : QuasiIsoAt I.ι (n + 1)
Tactic: rw [← quasiIsoAt_iff_exactAt I.ι (n + 1) (exactAt_succ_single_obj _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 2
have simp : n + 1 + 1 = n + 2
Tactic: simp only [CochainComplex.next]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ IsLimit I.kernelFork
have refine : I.kernelFork ≅ KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry
Tactic: refine IsLimit.ofIsoLimit (I.cocomplex.cyclesIsKernel 0 1 (by simp)) (Iso.symm ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ I.kernelFork ≅ KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯
have refine : CategoryStruct.comp (Y :=
    Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
      (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry))
    (Iso.hom
        (Iso.symm (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≪≫
          Iso.trans (Y := homology I.cocomplex 0) (isoOfQuasiIsoAt I.ι 0) (Iso.symm I.cocomplex.isoHomologyπ₀)) :
      I.kernelFork.pt ⟶
        Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
          (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry))
    (Fork.ι (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry) :
      Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
          (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry) ⟶
        I.cocomplex.X 0) =
  Fork.ι I.kernelFork
Tactic: refine Fork.ext ((singleObjHomologySelfIso _ _ _).symm ≪≫
    isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
        (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
      (Iso.hom
          (Iso.symm (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≪≫
            Iso.trans (Y := homology I.cocomplex 0) (isoOfQuasiIsoAt I.ι 0) (Iso.symm I.cocomplex.isoHomologyπ₀)) :
        I.kernelFork.pt ⟶
          Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
            (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
      (Fork.ι (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) :
        Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
            (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) ⟶
          I.cocomplex.X 0) =
    Fork.ι I.kernelFork
have rw : CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt) 0)
    (Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt))
    (Iso.hom (isoHomologyπ₀ (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt)) ≫
      Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≫
        CategoryStruct.comp (Y :=
          Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
            (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry))
          (Iso.hom
              (Iso.symm (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≪≫
                Iso.trans (Y := homology I.cocomplex 0) (isoOfQuasiIsoAt I.ι 0) (Iso.symm I.cocomplex.isoHomologyπ₀)) :
            I.kernelFork.pt ⟶
              Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
                (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry))
          (Fork.ι (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry) :
            Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
                (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) sorry) ⟶
              I.cocomplex.X 0)) =
  CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt) 0)
    (Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt))
    (Iso.hom (isoHomologyπ₀ (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt)) ≫
      Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≫ Fork.ι I.kernelFork)
Tactic: rw [← cancel_epi (singleObjHomologySelfIso (ComplexShape.up ℕ) _ _).hom,
    ← cancel_epi (isoHomologyπ₀ _).hom,
    ← cancel_epi (singleObjCyclesSelfIso (ComplexShape.up ℕ) _ _).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ Mono (I.ι.f n)
have zero : Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (I.ι.f 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
zero : Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (I.ι.f 0)
⊢ Mono (I.ι.f n)
have succ : ∀ (n : ℕ), Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) (I.ι.f (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) (I.ι.f (n + 1))
have succ : Mono.{v, u} (C := C) (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) (Y := I.cocomplex.X (n + 1)) 0
Tactic: rw [ι_f_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
⊢ Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) n)
have zero : Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
zero : Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
⊢ Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) n)
have succ : ∀ (n : ℕ), Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
⊢ Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
have succ : IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
Tactic: apply IsZero.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
⊢ IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
have succ : n + 1 ≠ 0
Tactic: apply HomologicalComplex.isZero_single_obj_X
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := ⋯
⊢ PreservesLimit (parallelPair f g) F
have this₁ : F.Additive
Tactic: haveI := additive_of_preservesBinaryBiproducts F