awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
g : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
      (Functor.obj shrinkYoneda.{max w' v, v, u} Y))
    (Functor.map uliftYoneda.{w', v, u} g ≫
      Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents
                (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
              Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents
                (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
              Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
          X) ≫
      Functor.map shrinkYoneda.{max w' v, v, u} g)
have w : ∀ (x : Cᵒᵖ) (x_1 : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) x),
  Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} Y) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map uliftYoneda.{w', v, u} g ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) sorry :
                    Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                      (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                Y))
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) sorry :
                    Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                      (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                X) ≫
            Functor.map shrinkYoneda.{max w' v, v, u} g)
          x))
      x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Y : Cᵒᵖ
X Y_1 : C
f : X ⟶ Y_1
⊢ Eq (α :=
    Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X ⟶
      Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1)
    (Functor.map (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
              ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                ULift.{w, v} (unop Y ⟶ X)))
          Y_1))
    (Iso.hom
        ((fun (X : C) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
              ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                ULift.{w, v} (unop Y ⟶ X)))
          X) ≫
      Functor.map (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) f)
have h : ∀
  (g :
    Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
      (Functor.obj shrinkYoneda.{w, v, u} X)),
  Eq (α := Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) f ≫
          Iso.hom
            ((fun (X : C) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                  ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                    ULift.{w, v} (unop Y ⟶ X)))
              Y_1)))
      { down := g :
        ULift.{v, w}
          (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
            (Functor.obj shrinkYoneda.{w, v, u} X)) })
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : C) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                  ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                    ULift.{w, v} (unop Y ⟶ X)))
              X) ≫
          Functor.map (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) f))
      { down := g :
        ULift.{v, w}
          (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
            (Functor.obj shrinkYoneda.{w, v, u} X)) })
Tactic: ext ⟨g⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sigma.Basic (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst_1 : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → Functor.{v₁, v₁, u₁, u₁} (C i) (D i)
α : (i : I) → F i ⟶ G i
i : I
X Y : C i
f : X ⟶ Y
⊢ (Functor.sigma (C := C) (D := D) F).map (SigmaHom.mk (C := C) f) ≫
      SigmaHom.mk (C := D)
        (NatTrans.app (α ((Sigma.mk (β := fun (i : I) ↦ C i) i Y).fst (β := fun (i : I) ↦ C i)))
          ((Sigma.mk (β := fun (i : I) ↦ C i) i Y).snd (β := fun (i : I) ↦ C i))) =
    SigmaHom.mk (C := D)
        (NatTrans.app (α ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i)))
          ((Sigma.mk (β := fun (i : I) ↦ C i) i X).snd (β := fun (i : I) ↦ C i))) ≫
      (Functor.sigma (C := C) (D := D) G).map (SigmaHom.mk (C := C) f)
have change : SigmaHom.mk (C := D)
    (Functor.map (F ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i))) f ≫
      NatTrans.app (α ((Sigma.mk (β := fun (i : I) ↦ C i) i Y).fst (β := fun (i : I) ↦ C i)))
        ((Sigma.mk (β := fun (i : I) ↦ C i) i Y).snd (β := fun (i : I) ↦ C i))) =
  SigmaHom.mk (C := D)
    (NatTrans.app (α ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i)))
        ((Sigma.mk (β := fun (i : I) ↦ C i) i X).snd (β := fun (i : I) ↦ C i)) ≫
      Functor.map (G ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i))) f)
Tactic: change SigmaHom.mk _ = SigmaHom.mk _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sigma.Basic (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst_1 : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → Functor.{v₁, v₁, u₁, u₁} (C i) (D i)
α : (i : I) → F i ⟶ G i
i : I
X Y : C i
f : X ⟶ Y
⊢ SigmaHom.mk (C := D)
      (Functor.map (F ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i))) f ≫
        NatTrans.app (α ((Sigma.mk (β := fun (i : I) ↦ C i) i Y).fst (β := fun (i : I) ↦ C i)))
          ((Sigma.mk (β := fun (i : I) ↦ C i) i Y).snd (β := fun (i : I) ↦ C i))) =
    SigmaHom.mk (C := D)
      (NatTrans.app (α ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i)))
          ((Sigma.mk (β := fun (i : I) ↦ C i) i X).snd (β := fun (i : I) ↦ C i)) ≫
        Functor.map (G ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i))) f)
have rw : SigmaHom.mk (C := D) ((α i).app ((Sigma.mk (β := fun (i : I) ↦ C i) i X).snd (β := fun (i : I) ↦ C i)) ≫ (G i).map f) =
  SigmaHom.mk (C := D)
    (NatTrans.app (α ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i)))
        ((Sigma.mk (β := fun (i : I) ↦ C i) i X).snd (β := fun (i : I) ↦ C i)) ≫
      Functor.map (G ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i))) f)
Tactic: rw [(α i).naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
⊢ IsIso f ↔ f ≠ 0
have mp : IsIso f → f ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
mp : IsIso f → f ≠ 0
⊢ IsIso f ↔ f ≠ 0
have mpr : f ≠ 0 → IsIso f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : IsIso f
w : f = 0
⊢ False
have j : IsIso (f ≫ i.hom)
Tactic: have j : IsIso (f ≫ i.hom) := by infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False
have j₁ : f ≫ i.hom ≠ 0
Tactic: rw [Simple.mono_isIso_iff_nonzero] at j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : f ≫ i.hom ≠ 0
⊢ False
have m₁ : Mono.{v, u} (C := C) (X := Y_1) (Y := X) 0
Tactic: subst w
Cleared hypotheses: f, m, h, w, j
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : f ≫ i.hom ≠ 0
m₁ : Mono.{v, u} (C := C) (X := Y_1) (Y := X) 0
⊢ False
have h₁ : IsIso.{v, u} (C := C) (X := Y_1) (Y := X) 0
Tactic: subst w
Cleared hypotheses: f, m, h, w, j
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : f ≫ i.hom ≠ 0
m₁ : Mono.{v, u} (C := C) (X := Y_1) (Y := X) 0
h₁ : IsIso.{v, u} (C := C) (X := Y_1) (Y := X) 0
⊢ False
have j₁ : Ne (α := Y_1 ⟶ Y) (0 ≫ i.hom) 0
Tactic: subst w
Cleared hypotheses: f, m, h, w, j
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : f ≠ 0
⊢ IsIso (f ≫ i.hom)
have w : f ≫ i.hom ≠ 0
Tactic: apply isIso_of_mono_of_nonzero
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ False
have w₁ : f = 0
Tactic: apply h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : f ≠ 0
⊢ IsIso f
have j : IsIso (f ≫ i.hom)
Tactic: have j : IsIso (f ≫ i.hom) := by
          apply isIso_of_mono_of_nonzero
          intro w
          apply h
          simpa using (cancel_mono i.inv).2 w
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
i : X ≅ Y
Y_1 : C
f : Y_1 ⟶ X
m : Mono f
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso f
have mpr : IsIso ((f ≫ i.hom) ≫ i.inv)
Tactic: rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} X
f : X ⟶ Y
inst_3 : HasKernel f
w : f ≠ 0
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0
have by_contra : ∀ (h : ¬Eq (α := kernel f ⟶ X) (kernel.ι f) 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} X
f : X ⟶ Y
inst_3 : HasKernel f
w : f ≠ 0
h : ¬Eq (α := kernel f ⟶ X) (kernel.ι f) 0
⊢ False
have this : IsIso (X := kernel f) (kernel.ι f)
Tactic: haveI := isIso_of_mono_of_nonzero h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} X
f : X ⟶ Y
inst_3 : HasKernel f
w : f ≠ 0
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0
have by_contra : ¬Eq (α := kernel f ⟶ X) (kernel.ι f) 0 → False
Tactic: classical
    by_contra h
    haveI := isIso_of_mono_of_nonzero h
    exact w (eq_zero_of_epi_kernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} X
f : X ⟶ Y
inst_3 : HasKernel f
w : f ≠ 0
by_contra by_contra₁ by_contra₂ : ∀ (h : ¬Eq (α := kernel f ⟶ X) (kernel.ι f) 0), False
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0
have by_contra₃ : ∀ (h : ¬Eq (α := kernel f ⟶ X) (kernel.ι f) 0) (this : IsIso (X := kernel f) (kernel.ι f)), False
Tactic: classical
    by_contra h
    haveI := isIso_of_mono_of_nonzero h
    exact w (eq_zero_of_epi_kernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasEqualizers.{v, u} C
X Y : C
inst_3 : Simple.{v, u} Y
f : X ⟶ Y
inst_4 : HasImage f
w : f ≠ 0
⊢ Epi f
have rw : Epi (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
Tactic: rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasEqualizers.{v, u} C
X Y : C
inst_3 : Simple.{v, u} Y
f : X ⟶ Y
inst_4 : HasImage f
w : f ≠ 0
⊢ Epi (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
have this : IsIso (X := image f) (image.ι f)
Tactic: haveI : IsIso (image.ι f) := isIso_of_mono_of_nonzero fun h => w (eq_zero_of_image_eq_zero h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
f : X ⟶ Y
inst_3 : Mono f
w : IsIso f → False
⊢ f = 0
have by_contra : ∀ (h : ¬f = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
f : X ⟶ Y
inst_3 : Mono f
w : IsIso f → False
⊢ f = 0
have by_contra : ¬f = 0 → False
Tactic: classical
    by_contra h
    exact w (isIso_of_mono_of_nonzero h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0
have mp : IsIso f → f ≠ 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
mp : IsIso f → f ≠ 0
⊢ IsIso f ↔ f ≠ 0
have mpr : f ≠ 0 → IsIso f
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
h_1 : IsIso f
⊢ f ≠ 0
have hx : Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
Tactic: have hx := cokernel.π_of_epi f
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h_1 : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
h_2 : IsIso f
hx : Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
h : f = 0
⊢ False
have I₁ : Mono.{v, u} (C := C) (X := Y) (Y := X) 0
Tactic: subst h
Cleared hypotheses: f, I, h_2, hx, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h_1 : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
h_2 : IsIso f
hx : Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
h : f = 0
I₁ : Mono.{v, u} (C := C) (X := Y) (Y := X) 0
⊢ False
have a : IsIso.{v, u} (C := C) (X := Y) (Y := X) 0
Tactic: subst h
Cleared hypotheses: f, I, h_2, hx, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h_1 : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
h_2 : IsIso f
hx : Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
h : f = 0
I₁ : Mono.{v, u} (C := C) (X := Y) (Y := X) 0
a : IsIso.{v, u} (C := C) (X := Y) (Y := X) 0
⊢ False
have hx₁ : Eq.{v + 1} (α := X ⟶ cokernel.{v, u} (X := Y) (Y := X) 0) (cokernel.π 0) 0
Tactic: subst h
Cleared hypotheses: f, I, h_2, hx, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ IsIso f
have mpr : Epi f
Tactic: suffices Epi f by exact isIso_of_mono_of_epi _
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ Epi f
have mpr : Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
Tactic: apply Preadditive.epi_of_cokernel_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
have mpr : ∀ (h' : ¬Eq (α := X ⟶ cokernel f) (cokernel.π f) 0), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0
have mp : IsIso f → f ≠ 0
Tactic: classical
      fconstructor
      · intros
        have hx := cokernel.π_of_epi f
        by_contra h
        subst h
        exact (h _).mp (cokernel.π_of_zero _ _) hx
      · intro hf
        suffices Epi f by exact isIso_of_mono_of_epi _
        apply Preadditive.epi_of_cokernel_zero
        by_contra h'
        exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
mp : IsIso f → f ≠ 0
⊢ IsIso f ↔ f ≠ 0
have mpr : f ≠ 0 → IsIso f
Tactic: classical
      fconstructor
      · intros
        have hx := cokernel.π_of_epi f
        by_contra h
        subst h
        exact (h _).mp (cokernel.π_of_zero _ _) hx
      · intro hf
        suffices Epi f by exact isIso_of_mono_of_epi _
        apply Preadditive.epi_of_cokernel_zero
        by_contra h'
        exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
f : X ⟶ Y
w : f ≠ 0
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
have by_contra : ∀ (h : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
f : X ⟶ Y
w : f ≠ 0
h : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
⊢ False
have this : IsIso (Y := cokernel f) (cokernel.π f)
Tactic: haveI := isIso_of_epi_of_nonzero h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
f : X ⟶ Y
w : f ≠ 0
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
have by_contra : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0 → False
Tactic: classical
    by_contra h
    haveI := isIso_of_epi_of_nonzero h
    exact w (eq_zero_of_mono_cokernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
inst_2 : Simple.{v, u} Y
f : X ⟶ Y
w : f ≠ 0
by_contra by_contra₁ by_contra₂ : ∀ (h : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), False
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
have by_contra₃ : ∀ (h : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0) (this : IsIso (Y := cokernel f) (cokernel.π f)), False
Tactic: classical
    by_contra h
    haveI := isIso_of_epi_of_nonzero h
    exact w (eq_zero_of_mono_cokernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
inst_2 : Simple.{v, u} X
f : X ⟶ Y
inst_3 : Epi f
w : IsIso f → False
⊢ f = 0
have by_contra : ∀ (h : ¬f = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
inst_2 : Simple.{v, u} X
f : X ⟶ Y
inst_3 : Epi f
w : IsIso f → False
⊢ f = 0
have by_contra : ¬f = 0 → False
Tactic: classical
    by_contra h
    exact w (isIso_of_epi_of_nonzero h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
⊢ IsIso.{v, u} (C := C) (X := X) (Y := biprod.{v, u} X Y) biprod.inl ↔ IsZero.{v, u} Y
have rw : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0 ↔ IsZero.{v, u} Y
Tactic: rw [biprod.isIso_inl_iff_id_eq_fst_comp_inl, ← biprod.total, add_eq_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0 ↔ IsZero.{v, u} Y
have mp : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0 → IsZero.{v, u} Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
mp : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0 → IsZero.{v, u} Y
⊢ Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0 ↔ IsZero.{v, u} Y
have mpr : IsZero.{v, u} Y → Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
h : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0
⊢ IsZero.{v, u} Y
have h₁ : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ Y)
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) biprod.snd)
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) 0 biprod.snd)
Tactic: replace h := h =≫ biprod.snd
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
h : IsZero.{v, u} Y
⊢ Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0
have h₁ : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ Y) biprod.snd 0
Tactic: rw [IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] at h
Cleared hypotheses: h