awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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 := over.{v, u} Z) (Projective.π Z)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Iso (C := ShortComplex.{v, u} C)
    (ShortComplex.mk (X₁ := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1) (X₂ :=
      HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0) (X₃ := Z) (HomologicalComplex.d (ofComplex Z) 1 0)
      (HomologicalComplex.Hom.f
          ((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 :
        HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶
          HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Z) 0)
      ⋯)
    (ShortComplex.mk (X₁ := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)) (Projective.π Z)
      ⋯)

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
          (by simp [ofComplex]) (by simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Eq.{v + 1} (α :=
    ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)) ⟶
      ShortComplex.X₃.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)))
    (ShortComplex.g (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)))
    0

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Eq.{v + 1} (α :=
    ShortComplex.X₁.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (ChainComplex.single₀ C) Z)) ⟶
      ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (ChainComplex.single₀ C) Z)))
    (ShortComplex.f
      (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
        (Functor.obj (ChainComplex.single₀ C) Z)))
    0

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Eq.{v + 1} (α :=
    ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (ChainComplex.single₀ C) Z)) ⟶
      ShortComplex.X₃.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (ChainComplex.single₀ C) Z)))
    (ShortComplex.g
      (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
        (Functor.obj (ChainComplex.single₀ C) Z)))
    0

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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)
succ₁ : HomologicalComplex.ExactAt.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) 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)

Tactic:
rw [quasiIsoAt_iff_exactAt']

Premises used: quasiIsoAt_iff_exactAt'
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt.{v, u, 0} (ofComplex Z) (n + 1)

Tactic:
apply ofComplex_exactAt_succ

Premises used: CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Z) (n + 1)

Tactic:
apply ChainComplex.exactAt_succ_single_obj

Premises used: ChainComplex.exactAt_succ_single_obj
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
a : Over.{v, u} P
⊢ (app f a).hom = a.hom ≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
P : C
f : Over.{v, u} P
⊢ 𝟙 f.left ≫ f.hom = 𝟙 f.left ≫ f.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
P : C
⊢ Symmetric (α := Over.{v, u} P) (PseudoEqual P)

Tactic:
fun _ _ ⟨R, p, q, ep, Eq, comm⟩ => ⟨R, q, p, Eq, ep, comm.symm⟩

Premises used: _private.0.CategoryTheory.Abelian.pseudoEqual_symm.match_1, Symmetric, CategoryTheory.Abelian.PseudoEqual, Exists.intro, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
⊢ IsTrans (Over.{v, u} P) (PseudoEqual P)

Tactic:
⟨fun f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩ ↦ ?_⟩

Premises used: _private.0.CategoryTheory.Abelian.pseudoEqual_symm.match_1, IsTrans.mk, CategoryTheory.Abelian.PseudoEqual
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
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
⊢ IsTrans (Over.{v, u} P) (PseudoEqual P)

Tactic:
refine ⟨fun f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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

Tactic:
⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q',
    epi_comp _ _, epi_comp _ _, ?_⟩

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.snd, CategoryTheory.epi_comp, CategoryTheory.Limits.pullback.fst, CategoryTheory.Abelian.PseudoEqual, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
refine : _root_.Eq (α := pullback q p' ⟶ P) ((pullback.fst q p' ≫ p) ≫ f.hom) ((pullback.snd q p' ≫ q') ≫ h.hom)
⊢ PseudoEqual P f h

Tactic:
refine ⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q',
    epi_comp _ _, epi_comp _ _, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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)
rw₆ 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)

Tactic:
rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
a : Q ⟶ P
⊢ Eq (α := Quot (α := Over.{v, u} P) (PseudoEqual P))
    (Quot.mk (PseudoEqual P) (Over.mk a) : Quot (α := Over.{v, u} P) (PseudoEqual P))
    (⟦Over.mk a⟧ : Quotient (α := Over.{v, u} P) (setoid P))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
rw rw₁ : q ≫ b.hom ≫ f = q ≫ b.hom ≫ f
⊢ p ≫ a.hom ≫ f = q ≫ b.hom ≫ f

Tactic:
rw [reassoc_of% comm]
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
a : Over.{v, u} P
⊢ Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) ⟦Over.mk (a.hom ≫ f)⟧

Tactic:
rfl

Premises used: Quotient.map, CategoryTheory.Abelian.app, rfl, CategoryTheory.Abelian.Pseudoelement.pseudoApply
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
simp : Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
⊢ 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))

Tactic:
simp only [app]

Premises used: CategoryTheory.Abelian.app
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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)
rw₁ rw₂ : (setoid R : Over R → Over R → Prop) (Over.mk ((x.hom ≫ f) ≫ g)) (Over.mk ((x.hom ≫ f) ≫ g))
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)

Tactic:
rw [← Category.assoc, Over.coe_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.coe_hom
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
⊢ Eq (α := Pseudoelement.{v, u} P → Pseudoelement.{v, u} R) (pseudoApply g ∘ pseudoApply f) (pseudoApply (f ≫ g))

Tactic:
funext fun _ => (comp_apply _ _ _).symm

Premises used: CategoryTheory.Abelian.Pseudoelement.comp_apply, funext, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : Over.{v, u} P
h : f ≈ Over.mk (Y := Q) 0
R : C
p : R ⟶ f.left
q : R ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit P) (Over.mk (Y := Q) 0)
w : Epi p
w_1 : Epi q
comm : p ≫ f.hom = q ≫ Over.hom (Over.mk (Y := Q) 0)
⊢ p ≫ f.hom = 0

Tactic:
simp [comm]
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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)
rw₃ rw₄ : Eq.{v + 1} (α := biprod.{v, u} f.left Q ⟶ P) 0 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)

Tactic:
rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]

Premises used: CategoryTheory.Over.coe_hom, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q R : C
⊢ Eq (α := Quotient (α := Over.{v, u} P) (setoid P)) ⟦Over.mk (Y := Q) 0⟧ ⟦Over.mk (Y := R) 0⟧

Tactic:
Quotient.sound <| (pseudoZero_aux R _).2 rfl

Premises used: Iff.mpr, CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux, Quotient.sound, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
⊢ Eq (α := Pseudoelement.{v, u} P) 0 ⟦Over.mk (Y := P) 0⟧

Tactic:
rfl

Premises used: CategoryTheory.Abelian.Pseudoelement.pseudoZero, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
⊢ Eq (α := Quotient (α := Over.{v, u} P) (setoid P)) ⟦Over.mk (Y := Q) 0⟧ 0

Tactic:
zero_eq_zero'

Premises used: CategoryTheory.Abelian.Pseudoelement.zero_eq_zero', CategoryTheory.Abelian.Pseudoelement.pseudoZero
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
a : Over.{v, u} P
rw : Eq (α := Quot (α := Over.{v, u} P) (PseudoEqual P)) (Quot.mk (PseudoEqual P) a) 0 ↔ a ≈ Over.mk (Y := P) 0
⊢ Eq (α := Quot (α := Over.{v, u} P) (PseudoEqual P)) (Quot.mk (PseudoEqual P) a) 0 ↔ a.hom = 0

Tactic:
rw [← pseudoZero_aux P a]

Premises used: CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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 ≈ Over.mk (Y := P) 0

Tactic:
Quotient.eq'

Premises used: Quotient.eq', Quotient, Quotient.mk', CategoryTheory.Abelian.Pseudoelement.pseudoZero
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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 ≈ Over.mk (Y := P) 0

Tactic:
exact Quotient.eq'

Premises used: Quotient.eq'
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
⊢ Eq (α := Pseudoelement.{v, u} Q)
    ⟦Over.mk (Y := Over.left.{v, u} (X := P) (Over.mk (Y := P) 0)) (Over.hom (Over.mk (Y := P) 0) ≫ f)⟧ 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
a : Pseudoelement.{v, u} P
a' : Over.{v, u} P
⊢ Eq (α := Pseudoelement.{v, u} Q) ⟦Over.mk (a'.hom ≫ 0)⟧ ⟦Over.mk (Y := Q) 0⟧

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
rw : 𝟙 P ≫ f = 0
⊢ f = 0

Tactic:
rw [← Category.id_comp f]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
⊢ 𝟙 P ≫ f = 0

Tactic:
(pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))

Premises used: CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff, CategoryTheory.Over.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.PseudoEqual, CategoryTheory.CategoryStruct.comp, Iff.mp, Quot.mk
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
⊢ 𝟙 P ≫ f = 0

Tactic:
exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))

Premises used: CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff, CategoryTheory.Over.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.PseudoEqual, CategoryTheory.CategoryStruct.comp, Iff.mp, Quot.mk
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
⊢ (∀ (a : Pseudoelement.{v, u} P), pseudoApply f a = 0) → 0 = f

Tactic:
Eq.symm ∘ zero_morphism_ext f

Premises used: Function.comp, CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
h : f = 0
a : Pseudoelement.{v, u} P
⊢ pseudoApply f a = 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
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'⟧
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'

Tactic:
induction abar, abar' using Quotient.inductionOn₂ with | _ a a'
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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'⟧

Tactic:
fun ha ↦ Quotient.sound ?_

Premises used: CategoryTheory.Abelian.Pseudoelement, Quotient.sound
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
h : ∀ (ha : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)), a ≈ a'
⊢ Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧) → Eq (α := Pseudoelement.{v, u} P) ⟦a⟧ ⟦a'⟧

Tactic:
refine fun ha ↦ Quotient.sound ?_

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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'⟧)
⊢ Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)

Tactic:
ha
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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'⟧)
⊢ Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (a.hom ≫ f)⟧ ⟦Over.mk (a'.hom ≫ f)⟧

Tactic:
convert!
    ha
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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'⟧)
⊢ 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
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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)⟧
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'
⊢ a ≈ a'

Tactic:
have ⟨R, p, q, ep, Eq, comm⟩ := Quotient.exact this
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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
simp : p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
⊢ (p ≫ a.hom) ≫ f = (q ≫ a'.hom) ≫ f

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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

Tactic:
comm

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
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

Tactic:
exact comm