awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
zero :
  QuasiIsoAt.{v, u, 0} (ι := ℕ) (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
        (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
          ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
      (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
          (Projective.π Z) ⋯ :
        { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
            0 }))
    0
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
        (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
          ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
      (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
          (Projective.π Z) ⋯ :
        { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
            0 }))
    n
have succ : ∀ (n : ℕ),
  QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
        (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
          ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
      (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
          (Projective.π Z) sorry :
        { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
            0 }))
    (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Epi.{v, u} (X :=
    ShortComplex.X₂.{v, u}
      (ShortComplex.mk (X₁ := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z))
        (Projective.π Z) ⋯))
    (ShortComplex.g
      (ShortComplex.mk (X₁ := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z))
        (Projective.π Z) ⋯))
have dsimp : Epi.{v, u} (X := over.{v, u} Z) (Projective.π Z)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
        (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
          ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
      (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
          (Projective.π Z) ⋯ :
        { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
            0 }))
    (n + 1)
have succ : HomologicalComplex.ExactAt.{v, u, 0} (ofComplex Z) (n + 1)
Tactic: rw [quasiIsoAt_iff_exactAt']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
succ : HomologicalComplex.ExactAt.{v, u, 0} (ofComplex Z) (n + 1)
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
        (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
          ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
      (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
          (Projective.π Z) ⋯ :
        { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
            0 }))
    (n + 1)
have succ₁ : HomologicalComplex.ExactAt.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Z) (n + 1)
Tactic: rw [quasiIsoAt_iff_exactAt']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
⊢ IsTrans (Over.{v, u} P) (PseudoEqual P)
have refine : ∀ (f g h : Over.{v, u} P),
  PseudoEqual P f g →
    PseudoEqual P g h →
      ∀ (R : C) (p : R ⟶ f.left) (q : R ⟶ g.left) (ep : Epi p) (Eq : Epi q) (comm : p ≫ f.hom = q ≫ g.hom) (R' : C)
        (p' : R' ⟶ g.left) (q' : R' ⟶ h.left) (ep' : Epi p') (eq' : Epi q') (comm' : p' ≫ g.hom = q' ≫ h.hom),
        PseudoEqual P f h
Tactic: refine ⟨fun f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h
have refine : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
Tactic: refine ⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q',
    epi_comp _ _, epi_comp _ _, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
have rw : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ p ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
Tactic: rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
rw : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ p ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
⊢ _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
have rw₁ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ q ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
Tactic: rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
rw : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ p ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₁ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ q ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
⊢ _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
have rw₂ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ q) ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
Tactic: rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
rw : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ p ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₁ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ q ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₂ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ q) ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
⊢ _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
have rw₃ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.snd q p' ≫ p') ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
Tactic: rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
rw : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ p ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₁ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ q ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₂ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ q) ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₃ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.snd q p' ≫ p') ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
⊢ _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
have rw₄ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.snd q p' ≫ p' ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
Tactic: rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
rw : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ p ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₁ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ q ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₂ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ q) ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₃ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.snd q p' ≫ p') ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₄ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.snd q p' ≫ p' ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
⊢ _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
have rw₅ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.snd q p' ≫ q' ≫ h.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
Tactic: rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
f g h : Over.{v, u} P
h_1 : PseudoEqual P f g
h_2 : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
rw : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ p ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₁ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.fst q p' ≫ q ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₂ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ q) ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₃ : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.snd q p' ≫ p') ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₄ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.snd q p' ≫ p' ≫ g.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
rw₅ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.snd q p' ≫ q' ≫ h.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
⊢ _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
have rw₆ : _root_.Eq (α := pullback q p' ⟶ P) (pullback.snd q p' ≫ q' ≫ h.hom) (pullback.snd q p' ≫ q' ≫ h.hom)
Tactic: rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
a b : Over.{v, u} P
h : a ≈ b
R : C
p : R ⟶ a.left
q : R ⟶ b.left
ep : Epi p
Eq : Epi q
comm : p ≫ a.hom = q ≫ b.hom
⊢ p ≫ a.hom ≫ f = q ≫ b.hom ≫ f
have rw : q ≫ b.hom ≫ f = q ≫ b.hom ≫ f
Tactic: rw [reassoc_of% comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement.{v, u} P
x : Over.{v, u} P
⊢ HasEquiv.Equiv (α := Over.{v, u} R) ((fun (g_1 : Over.{v, u} P) ↦ app (f ≫ g) g_1) x)
    ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) ((fun (g : Over.{v, u} P) ↦ app f g) x))
have simp : Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
Tactic: simp only [app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement.{v, u} P
x : Over.{v, u} P
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
have rw : Over.mk ((x.hom ≫ f) ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
Tactic: rw [← Category.assoc, Over.coe_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement.{v, u} P
x : Over.{v, u} P
rw : Over.mk ((x.hom ≫ f) ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
have rw₁ : (setoid R : Over R → Over R → Prop) (Over.mk ((x.hom ≫ f) ≫ g)) (Over.mk ((x.hom ≫ f) ≫ g))
Tactic: rw [← Category.assoc, Over.coe_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : Over.{v, u} P
hf : f.hom = 0
⊢ Eq (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ f.hom : biprod.{v, u} f.left Q ⟶ P)
    (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
have rw : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ 0 : biprod.{v, u} f.left Q ⟶ P)
  (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
Tactic: rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : Over.{v, u} P
hf : f.hom = 0
rw :
  Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ 0 : biprod.{v, u} f.left Q ⟶ P)
    (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
⊢ Eq (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ f.hom : biprod.{v, u} f.left Q ⟶ P)
    (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
have rw₁ : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ 0) (biprod.snd ≫ 0)
Tactic: rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : Over.{v, u} P
hf : f.hom = 0
rw :
  Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ 0 : biprod.{v, u} f.left Q ⟶ P)
    (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
rw₁ : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ 0) (biprod.snd ≫ 0)
⊢ Eq (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ f.hom : biprod.{v, u} f.left Q ⟶ P)
    (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
have rw₂ : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) 0 (biprod.snd ≫ 0)
Tactic: rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : Over.{v, u} P
hf : f.hom = 0
rw :
  Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ 0 : biprod.{v, u} f.left Q ⟶ P)
    (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
rw₁ : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ 0) (biprod.snd ≫ 0)
rw₂ : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) 0 (biprod.snd ≫ 0)
⊢ Eq (α := biprod.{v, u} f.left Q ⟶ P) (biprod.fst ≫ f.hom : biprod.{v, u} f.left Q ⟶ P)
    (biprod.snd ≫ Over.hom (Over.mk (Y := Q) 0) : biprod.{v, u} f.left Q ⟶ P)
have rw₃ : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) 0 0
Tactic: rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
a : Over.{v, u} P
⊢ Eq (α := Quot (α := Over.{v, u} P) (PseudoEqual P)) (Quot.mk (PseudoEqual P) a) 0 ↔ a.hom = 0
have rw : Eq (α := Quot (α := Over.{v, u} P) (PseudoEqual P)) (Quot.mk (PseudoEqual P) a) 0 ↔ a ≈ Over.mk (Y := P) 0
Tactic: rw [← pseudoZero_aux P a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement.{v, u} P), pseudoApply f a = 0
⊢ f = 0
have rw : 𝟙 P ≫ f = 0
Tactic: rw [← Category.id_comp f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Mono f
abar abar' : Pseudoelement.{v, u} P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'
have h : ∀ (a a' : Over.{v, u} P),
  Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧) → Eq (α := Pseudoelement.{v, u} P) ⟦a⟧ ⟦a'⟧
Tactic: induction abar, abar' using Quotient.inductionOn₂ with | _ a a'
Cleared hypotheses: abar, abar'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Mono f
a a' : Over.{v, u} P
⊢ Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧) → Eq (α := Pseudoelement.{v, u} P) ⟦a⟧ ⟦a'⟧
have h : ∀ (ha : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)), a ≈ a'
Tactic: refine fun ha ↦ Quotient.sound ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Mono f
a a' : Over.{v, u} P
ha : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
⊢ a ≈ a'
have this : Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (a.hom ≫ f)⟧ ⟦Over.mk (a'.hom ≫ f)⟧
Tactic: have : (⟦(a.hom ≫ f : Over Q)⟧ : Quotient (setoid Q)) = ⟦↑(a'.hom ≫ f)⟧ := by convert!
    ha
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Mono f
a a' : Over.{v, u} P
ha : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
this : Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (a.hom ≫ f)⟧ ⟦Over.mk (a'.hom ≫ f)⟧
⊢ a ≈ a'
have h : ∀ (R : C) (p : R ⟶ (Over.mk (a.hom ≫ f)).left) (q : R ⟶ (Over.mk (a'.hom ≫ f)).left) (ep : Epi p) (Eq : Epi q)
  (comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom), a ≈ a'
Tactic: have ⟨R, p, q, ep, Eq, comm⟩ := Quotient.exact this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Mono f
a a' : Over.{v, u} P
ha : _root_.Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
this : _root_.Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (a.hom ≫ f)⟧ ⟦Over.mk (a'.hom ≫ f)⟧
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ (p ≫ a.hom) ≫ f = (q ≫ a'.hom) ≫ f
have simp : p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
h : Function.Injective (α := Pseudoelement.{v, u} P) (pseudoApply f)
a : Pseudoelement.{v, u} P
ha : pseudoApply f a = 0
⊢ a = 0
have ha₁ : pseudoApply f a = pseudoApply f 0
Tactic: rw [← apply_zero f] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : Epi f
qbar : Pseudoelement.{v, u} Q
q : Over.{v, u} Q
⊢ 𝟙 (pullback f q.hom) ≫
      Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) =
    pullback.snd f q.hom ≫ q.hom
have rw : Eq.{v + 1} (α := pullback f q.hom ⟶ Q)
  (Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) :
    Over.left.{v, u} (X := Q)
        ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) ⟶
      Q)
  (pullback.snd f q.hom ≫ q.hom)
Tactic: rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]