awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
i : I
X : C i
⊢ (inclDesc (C := C) F i).hom.app X = 𝟙 ((F i).obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
i : I
X : C i
⊢ (inclDesc (C := C) F i).inv.app X = 𝟙 ((F i).obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
q : (i : I) × C i ⥤ D
h : (i : I) → incl (C := C) i ⋙ q ≅ F i
i : I
X Y : C i
f : X ⟶ Y
⊢ q.map (SigmaHom.mk (C := C) f) ≫
      Iso.hom
        ((fun (x : (i : I) × C i) ↦
            (match (motive := (x : (i : I) × C i) → q.obj x ≅ (desc (C := C) F).obj x) x with
              | ⟨i, X⟩ => (h i).app X :
              q.obj x ≅ (desc (C := C) F).obj x))
          (Sigma.mk (β := fun (i : I) ↦ C i) i Y)) =
    Iso.hom
        ((fun (x : (i : I) × C i) ↦
            (match (motive := (x : (i : I) × C i) → q.obj x ≅ (desc (C := C) F).obj x) x with
              | ⟨i, X⟩ => (h i).app X :
              q.obj x ≅ (desc (C := C) F).obj x))
          (Sigma.mk (β := fun (i : I) ↦ C i) i X)) ≫
      (desc (C := C) F).map (SigmaHom.mk (C := C) f)

Tactic:
apply (h i).hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
q : (i : I) × C i ⥤ D
h : (i : I) → incl (C := C) i ⋙ q ≅ F i
i : I
X : C i
⊢ (descUniq (C := C) F q h).hom.app (Sigma.mk (β := fun (i : I) ↦ C i) i X) = (h i).hom.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
q : (i : I) × C i ⥤ D
h : (i : I) → incl (C := C) i ⋙ q ≅ F i
i : I
X : C i
⊢ (descUniq (C := C) F q h).inv.app (Sigma.mk (β := fun (i : I) ↦ C i) i X) = (h i).inv.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₂
g : J → I
j : J
X : C (g j)
⊢ Functor.obj (map C g) (Sigma.mk (β := fun (j : J) ↦ C (g j)) j X) = Sigma.mk (β := fun (i : I) ↦ C i) (g j) X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₂
g : J → I
j : J
X Y : C (g j)
f : X ⟶ Y
⊢ Functor.map (map C g) (SigmaHom.mk (C := fun (j : J) ↦ C (g j)) f) = SigmaHom.mk (C := C) f

Tactic:
rfl

Premises used: CategoryTheory.Sigma.descMap, rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
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
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)
⊢ (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)

Tactic:
change SigmaHom.mk _ = SigmaHom.mk _

Premises used: CategoryTheory.Sigma.SigmaHom.mk
-- Module: Mathlib.CategoryTheory.Sigma.Basic
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
rw 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)
⊢ 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:
rw [(α i).naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Simple
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 : f ≠ 0
⊢ IsIso f

Tactic:
(Simple.mono_isIso_iff_nonzero f).mpr w

Premises used: Iff.mpr, CategoryTheory.Simple.mono_isIso_iff_nonzero
-- Module: Mathlib.CategoryTheory.Simple
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
mpr : f ≠ 0 → IsIso f
⊢ IsIso f ↔ f ≠ 0

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ IsIso (f ≫ i.hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ IsIso (f ≫ i.hom)

Tactic:
have j : IsIso (f ≫ i.hom) := by infer_instance
-- Module: Mathlib.CategoryTheory.Simple
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)
⊢ f ≫ i.hom ≠ 0

Tactic:
rw [Simple.mono_isIso_iff_nonzero] at j

Premises used: CategoryTheory.Simple.mono_isIso_iff_nonzero
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ Mono.{v, u} (C := C) (X := Y_1) (Y := X) 0

Tactic:
subst w
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ IsIso.{v, u} (C := C) (X := Y_1) (Y := X) 0

Tactic:
subst w
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ Ne (α := Y_1 ⟶ Y) (0 ≫ i.hom) 0

Tactic:
subst w
-- Module: Mathlib.CategoryTheory.Simple
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
m : Mono.{v, u} (C := C) (X := Y_1) (Y := X) 0
h : IsIso.{v, u} (C := C) (X := Y_1) (Y := X) 0
j : Ne (α := Y_1 ⟶ Y) (0 ≫ i.hom) 0
⊢ False

Tactic:
simp at j
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ IsIso (f ≫ i.hom)

Tactic:
apply isIso_of_mono_of_nonzero

Premises used: CategoryTheory.isIso_of_mono_of_nonzero
-- Module: Mathlib.CategoryTheory.Simple
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
w₁ : f = 0
⊢ False

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ f = 0

Tactic:
simpa using (cancel_mono i.inv).2 w

Premises used: Iff.mpr, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Simple
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)

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
-- Module: Mathlib.CategoryTheory.Simple
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)
mpr : IsIso ((f ≫ i.hom) ≫ i.inv)
⊢ IsIso f

Tactic:
rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Simple
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 ≫ i.hom) ≫ i.inv)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
i : X ≅ Y
⊢ Simple.{v, u} X ↔ Simple.{v, u} Y

Tactic:
⟨fun _ => Simple.of_iso i.symm, fun _ => Simple.of_iso i⟩

Premises used: CategoryTheory.Simple.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Simple
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 : ∀ (h : ¬Eq (α := kernel f ⟶ X) (kernel.ι f) 0), False
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0

Tactic:
by_contra h
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ IsIso (X := kernel f) (kernel.ι f)

Tactic:
haveI := isIso_of_mono_of_nonzero h
-- Module: Mathlib.CategoryTheory.Simple
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
this : IsIso (X := kernel f) (kernel.ι f)
⊢ False

Tactic:
w (eq_zero_of_epi_kernel f)

Premises used: CategoryTheory.Limits.eq_zero_of_epi_kernel
-- Module: Mathlib.CategoryTheory.Simple
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
this : IsIso (X := kernel f) (kernel.ι f)
⊢ False

Tactic:
exact w (eq_zero_of_epi_kernel f)

Premises used: CategoryTheory.Limits.eq_zero_of_epi_kernel
-- Module: Mathlib.CategoryTheory.Simple
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
by_contra₃ : ∀ (h : ¬Eq (α := kernel f ⟶ X) (kernel.ι f) 0) (this : IsIso (X := kernel f) (kernel.ι f)), False
⊢ Eq (α := kernel f ⟶ X) (kernel.ι f) 0

Tactic:
classical
    by_contra h
    haveI := isIso_of_mono_of_nonzero h
    exact w (eq_zero_of_epi_kernel f)
-- Module: Mathlib.CategoryTheory.Simple
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
rw : Epi (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
⊢ Epi f

Tactic:
rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ 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)
-- Module: Mathlib.CategoryTheory.Simple
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
this : IsIso (X := image f) (image.ι f)
⊢ Epi (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.Simple
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
by_contra : ∀ (h : ¬f = 0), False
⊢ f = 0

Tactic:
by_contra h
-- Module: Mathlib.CategoryTheory.Simple
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
h : ¬f = 0
⊢ False

Tactic:
w (isIso_of_mono_of_nonzero h)

Premises used: CategoryTheory.isIso_of_mono_of_nonzero
-- Module: Mathlib.CategoryTheory.Simple
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
h : ¬f = 0
⊢ False

Tactic:
exact w (isIso_of_mono_of_nonzero h)

Premises used: CategoryTheory.isIso_of_mono_of_nonzero
-- Module: Mathlib.CategoryTheory.Simple
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
by_contra by_contra₁ by_contra₂ : ∀ (h : ¬f = 0), False
⊢ f = 0

Tactic:
classical
    by_contra h
    exact w (isIso_of_mono_of_nonzero h)
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
inst_2 : Simple.{v, u} X
⊢ IsIso.{v, u} (𝟙 X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
inst_2 : Simple.{v, u} X
⊢ Nontrivial.{v} (End X)

Tactic:
nontrivial_of_ne 1 _ (id_nonzero X)

Premises used: nontrivial_of_ne, CategoryTheory.id_nonzero, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
inst_2 : Simple.{v, u} X
⊢ ¬IsZero.{v, u} X

Tactic:
simpa [Limits.IsZero.iff_id_eq_zero] using id_nonzero X

Premises used: CategoryTheory.id_nonzero, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : Simple.{v, u} (C := C) 0
⊢ Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := C) 0 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 0) ∧
    Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := C) 0 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Simple
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
mpr : f ≠ 0 → IsIso f
⊢ IsIso f ↔ f ≠ 0

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ Eq (α := X ⟶ cokernel f) (cokernel.π f) 0

Tactic:
have hx := cokernel.π_of_epi f
-- Module: Mathlib.CategoryTheory.Simple
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
hx : Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
mp : ∀ (h : f = 0), False
⊢ f ≠ 0

Tactic:
by_contra h
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ Mono.{v, u} (C := C) (X := Y) (Y := X) 0

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ IsIso.{v, u} (C := C) (X := Y) (Y := X) 0

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ Eq.{v + 1} (α := X ⟶ cokernel.{v, u} (X := Y) (Y := X) 0) (cokernel.π 0) 0

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Simple
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
I : Mono.{v, u} (C := C) (X := Y) (Y := X) 0
h_1 : IsIso.{v, u} (C := C) (X := Y) (Y := X) 0
hx : Eq.{v + 1} (α := X ⟶ cokernel.{v, u} (X := Y) (Y := X) 0) (cokernel.π 0) 0
⊢ False

Tactic:
(h _).mp (cokernel.π_of_zero _ _) hx

Premises used: CategoryTheory.Limits.cokernel.π_of_zero, Iff.mp
-- Module: Mathlib.CategoryTheory.Simple
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
I : Mono.{v, u} (C := C) (X := Y) (Y := X) 0
h_1 : IsIso.{v, u} (C := C) (X := Y) (Y := X) 0
hx : Eq.{v + 1} (α := X ⟶ cokernel.{v, u} (X := Y) (Y := X) 0) (cokernel.π 0) 0
⊢ False

Tactic:
exact (h _).mp (cokernel.π_of_zero _ _) hx

Premises used: CategoryTheory.Limits.cokernel.π_of_zero, Iff.mp
-- Module: Mathlib.CategoryTheory.Simple
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
this : Epi f
⊢ IsIso f

Tactic:
isIso_of_mono_of_epi _

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Simple
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
this : Epi f
⊢ IsIso f

Tactic:
exact isIso_of_mono_of_epi _

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Simple
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
mpr : Epi f
⊢ IsIso f

Tactic:
suffices Epi f by exact isIso_of_mono_of_epi _
-- Module: Mathlib.CategoryTheory.Simple
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
mpr : Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
⊢ Epi f

Tactic:
apply Preadditive.epi_of_cokernel_zero

Premises used: CategoryTheory.Preadditive.epi_of_cokernel_zero
-- Module: Mathlib.CategoryTheory.Simple
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
mpr : ∀ (h' : ¬Eq (α := X ⟶ cokernel f) (cokernel.π f) 0), False
⊢ Eq (α := X ⟶ cokernel f) (cokernel.π f) 0

Tactic:
by_contra h'
-- Module: Mathlib.CategoryTheory.Simple
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
h' : ¬Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
⊢ False

Tactic:
cokernel_not_iso_of_nonzero hf ((h _).mpr h')

Premises used: Iff.mpr, CategoryTheory.Limits.cokernel_not_iso_of_nonzero
-- Module: Mathlib.CategoryTheory.Simple
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
h' : ¬Eq (α := X ⟶ cokernel f) (cokernel.π f) 0
⊢ False

Tactic:
exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')

Premises used: Iff.mpr, CategoryTheory.Limits.cokernel_not_iso_of_nonzero
-- Module: Mathlib.CategoryTheory.Simple
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
mpr mpr₁ : f ≠ 0 → IsIso f
⊢ 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')

Premises used: CategoryTheory.Preadditive.epi_of_cokernel_zero
-- Module: Mathlib.CategoryTheory.Simple
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 : f ≠ 0
⊢ IsIso f

Tactic:
haveI : Mono f :=
    Preadditive.mono_of_kernel_zero (mono_to_simple_zero_of_not_iso (kernel_not_iso_of_nonzero w))
  isIso_of_mono_of_epi f

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Simple
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 : ∀ (h : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), False
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0

Tactic:
by_contra h
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ IsIso (Y := cokernel f) (cokernel.π f)

Tactic:
haveI := isIso_of_epi_of_nonzero h
-- Module: Mathlib.CategoryTheory.Simple
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
this : IsIso (Y := cokernel f) (cokernel.π f)
⊢ False

Tactic:
w (eq_zero_of_mono_cokernel f)

Premises used: CategoryTheory.Limits.eq_zero_of_mono_cokernel