awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact w (eq_zero_of_mono_cokernel f)

Premises used: CategoryTheory.Limits.eq_zero_of_mono_cokernel
-- 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 by_contra₁ by_contra₂ : ∀ (h : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0), False
by_contra₃ : ∀ (h : ¬Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0) (this : IsIso (Y := cokernel f) (cokernel.π f)), False
⊢ Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0

Tactic:
classical
    by_contra h
    haveI := isIso_of_epi_of_nonzero h
    exact w (eq_zero_of_mono_cokernel f)
-- 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 : 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 : Abelian.{v, u} C
X Y : C
inst_2 : Simple.{v, u} X
f : X ⟶ Y
inst_3 : Epi f
w : IsIso f → False
h : ¬f = 0
⊢ False

Tactic:
w (isIso_of_epi_of_nonzero h)

Premises used: CategoryTheory.isIso_of_epi_of_nonzero
-- 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 : IsIso f → False
h : ¬f = 0
⊢ False

Tactic:
exact w (isIso_of_epi_of_nonzero h)

Premises used: CategoryTheory.isIso_of_epi_of_nonzero
-- 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 : IsIso f → False
by_contra by_contra₁ by_contra₂ : ∀ (h : ¬f = 0), False
⊢ f = 0

Tactic:
classical
    by_contra h
    exact w (isIso_of_epi_of_nonzero h)
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
rw : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0 ↔ IsZero.{v, u} Y
⊢ IsIso.{v, u} (C := C) (X := X) (Y := biprod.{v, u} X Y) biprod.inl ↔ IsZero.{v, u} Y

Tactic:
rw [biprod.isIso_inl_iff_id_eq_fst_comp_inl, ← biprod.total, add_eq_left]

Premises used: CategoryTheory.Limits.biprod.total, add_eq_left, CategoryTheory.Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl
-- Module: Mathlib.CategoryTheory.Simple
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
mpr : IsZero.{v, u} Y → Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0
⊢ Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0 ↔ IsZero.{v, u} Y

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Simple
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Simple
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 ⟶ 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)
⊢ IsZero.{v, u} Y

Tactic:
simpa [← IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h

Premises used: CategoryTheory.Limits.biprod.snd, CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero
-- Module: Mathlib.CategoryTheory.Simple
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 ⟶ Y) biprod.snd 0

Tactic:
rw [IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] at h

Premises used: CategoryTheory.Limits.biprod.snd, CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero
-- Module: Mathlib.CategoryTheory.Simple
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 ⟶ Y) biprod.snd 0
mpr : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (0 ≫ biprod.inr) 0
mpr₁ mpr₂ : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) 0 0
⊢ Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0

Tactic:
rw [h, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
⊢ IsZero.{v, u} Y ∨ IsZero.{v, u} Z

Tactic:
or_iff_not_imp_left.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
refine : ∀ (h : ¬IsZero.{v, u} Y), IsZero.{v, u} Z
⊢ IsZero.{v, u} Y ∨ IsZero.{v, u} Z

Tactic:
refine or_iff_not_imp_left.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : ¬IsZero.{v, u} Y
⊢ ¬Eq.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0

Tactic:
rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h

Premises used: CategoryTheory.Limits.biprod.inl, CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : ¬Eq.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
⊢ Ne.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0

Tactic:
change biprod.inl ≠ 0 at h

Premises used: CategoryTheory.Limits.biprod.inl
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : Ne.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
⊢ Simple.{v, u} (biprod.{v, u} Y Z)

Tactic:
have : Simple (Y ⊞ Z) := Simple.of_iso i.symm
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : Ne.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
this : Simple.{v, u} (biprod.{v, u} Y Z)
⊢ IsIso.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl

Tactic:
rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h

Premises used: CategoryTheory.Simple.mono_isIso_iff_nonzero, CategoryTheory.Limits.biprod.inl
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : Ne.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
this : Simple.{v, u} (biprod.{v, u} Y Z)
h₁ : IsIso.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl
⊢ Simple.{v, u} (biprod.{v, u} Y Z)

Tactic:
rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h

Premises used: CategoryTheory.Simple.mono_isIso_iff_nonzero, CategoryTheory.Limits.biprod.inl
-- Module: Mathlib.CategoryTheory.Simple
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : IsIso.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl
this : Simple.{v, u} (biprod.{v, u} Y Z)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : IsZero.{v, u} Z) (this : Simple.{v, u} (biprod.{v, u} Y Z)), IsZero.{v, u} Z
⊢ IsZero.{v, u} Z

Tactic:
rwa [Biprod.isIso_inl_iff_isZero] at h

Premises used: CategoryTheory.Biprod.isIso_inl_iff_isZero
-- 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
X : C
inst_3 : Simple.{v, u} X
⊢ Nontrivial (Subobject.{v, u} X)

Tactic:
nontrivial_of_not_isZero (Simple.not_isZero X)

Premises used: CategoryTheory.Subobject.nontrivial_of_not_isZero, CategoryTheory.Simple.not_isZero
-- 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
X : C
inst_3 : Simple.{v, u} X
a : Subobject.{v, u} X
obtain : ∀ (Y : C) (i : Y ⟶ X) (w : Mono i), mk i = ⊥ ∨ mk i = ⊤
⊢ a = ⊥ ∨ a = ⊤

Tactic:
obtain ⟨Y, i, _, rfl⟩ := Subobject.mk_surjective a

Premises used: CategoryTheory.Subobject.mk_surjective, rfl
-- 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
X : C
inst_3 : Simple.{v, u} X
Y : C
i : Y ⟶ X
w : Mono i
pos : ∀ (h : i = 0), mk i = ⊥ ∨ mk i = ⊤
neg : ∀ (h : ¬i = 0), mk i = ⊥ ∨ mk i = ⊤
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
by_cases h : i = 0
-- 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
X : C
inst_3 : Simple.{v, u} X
Y : C
i : Y ⟶ X
w : Mono i
h : i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
Or.inl (mk_eq_bot_iff_zero.mpr h)

Premises used: Iff.mpr, CategoryTheory.Subobject.mk_eq_bot_iff_zero, Or.inl
-- 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
X : C
inst_3 : Simple.{v, u} X
Y : C
i : Y ⟶ X
w : Mono i
h : i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
exact Or.inl (mk_eq_bot_iff_zero.mpr h)

Premises used: Iff.mpr, CategoryTheory.Subobject.mk_eq_bot_iff_zero, Or.inl
-- 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
X : C
inst_3 : Simple.{v, u} X
Y : C
i : Y ⟶ X
w : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
Or.inr ((isIso_iff_mk_eq_top _).mp ((Simple.mono_isIso_iff_nonzero i).mpr h))

Premises used: Iff.mpr, CategoryTheory.Simple.mono_isIso_iff_nonzero, Iff.mp, CategoryTheory.Subobject.isIso_iff_mk_eq_top, Or.inr
-- 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
X : C
inst_3 : Simple.{v, u} X
Y : C
i : Y ⟶ X
w : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
exact Or.inr ((isIso_iff_mk_eq_top _).mp ((Simple.mono_isIso_iff_nonzero i).mpr h))

Premises used: Iff.mpr, CategoryTheory.Simple.mono_isIso_iff_nonzero, Iff.mp, CategoryTheory.Subobject.isIso_iff_mk_eq_top, Or.inr
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
mono_isIso_iff_nonzero : ∀ {Y : C} (f : Y ⟶ X) [Mono f], IsIso f ↔ f ≠ 0
⊢ Simple.{v, u} X

Tactic:
constructor
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
mono_isIso_iff_nonzero : IsIso f → f ≠ 0
mono_isIso_iff_nonzero₁ : 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
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : IsIso f
⊢ mk f = ⊤

Tactic:
rw [Subobject.isIso_iff_mk_eq_top] at i

Premises used: CategoryTheory.Subobject.isIso_iff_mk_eq_top
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : f = 0
⊢ mk f = ⊥

Tactic:
rw [← Subobject.mk_eq_bot_iff_zero] at w

Premises used: CategoryTheory.Subobject.mk_eq_bot_iff_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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : mk f = ⊥
⊢ False

Tactic:
IsSimpleOrder.bot_ne_top (w.symm.trans i)

Premises used: IsSimpleOrder.bot_ne_top, Eq.symm, Eq.trans
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : mk f = ⊥
⊢ False

Tactic:
exact IsSimpleOrder.bot_ne_top (w.symm.trans i)

Premises used: IsSimpleOrder.bot_ne_top, Eq.symm, Eq.trans
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
mono_isIso_iff_nonzero : ∀ (h : mk f = ⊥), IsIso f
mono_isIso_iff_nonzero₁ : ∀ (h : mk f = ⊤), IsIso f
⊢ IsIso f

Tactic:
rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)

Premises used: CategoryTheory.Subobject.mk, IsSimpleOrder.eq_bot_or_eq_top
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ f = 0

Tactic:
rw [Subobject.mk_eq_bot_iff_zero] at h

Premises used: CategoryTheory.Subobject.mk_eq_bot_iff_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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : f = 0
⊢ IsIso f

Tactic:
False.elim (i h)

Premises used: False.elim
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : f = 0
⊢ IsIso f

Tactic:
exact False.elim (i h)

Premises used: False.elim
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f

Tactic:
(Subobject.isIso_iff_mk_eq_top _).mpr h

Premises used: Iff.mpr, CategoryTheory.Subobject.isIso_iff_mk_eq_top
-- 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
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f

Tactic:
exact (Subobject.isIso_iff_mk_eq_top _).mpr h

Premises used: Iff.mpr, CategoryTheory.Subobject.isIso_iff_mk_eq_top
-- 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
X : C
h : Simple.{v, u} X
⊢ IsSimpleOrder (Subobject.{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
inst_2 : HasZeroObject.{v, u} C
X : C
h : IsSimpleOrder (Subobject.{v, u} X)
⊢ Simple.{v, u} X

Tactic:
simple_of_isSimpleOrder_subobject X

Premises used: CategoryTheory.simple_of_isSimpleOrder_subobject
-- 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
X : C
h : IsSimpleOrder (Subobject.{v, u} X)
⊢ Simple.{v, u} X

Tactic:
exact simple_of_isSimpleOrder_subobject X

Premises used: CategoryTheory.simple_of_isSimpleOrder_subobject
-- 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
X : C
Y : Subobject.{v, u} X
⊢ Simple.{v, u} (Functor.obj underlying Y) ↔ IsAtom Y

Tactic:
(simple_iff_subobject_isSimpleOrder _).trans
    ((OrderIso.isSimpleOrder_iff (subobjectOrderIso Y)).trans Set.isSimpleOrder_Iic_iff_isAtom)

Premises used: CategoryTheory.simple_iff_subobject_isSimpleOrder, Set.isSimpleOrder_Iic_iff_isAtom, CategoryTheory.Subobject.subobjectOrderIso, OrderIso.isSimpleOrder_iff, Iff.trans
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
x : SingleObj M
⊢ Eq.{u + 1} (α := x ⟶ x) (𝟙 x) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
x y z : SingleObj M
f : x ⟶ y
g : y ⟶ z
⊢ f ≫ g = g * f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
G : Type u
inst : Group G
x y : SingleObj G
f : x ⟶ y
hom_inv_id : Eq.{u + 1} (α := x ⟶ x) (f ≫ f⁻¹) (𝟙 x)
⊢ inv f = f⁻¹

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
G : Type u
inst : Group G
x y : SingleObj G
f : x ⟶ y
hom_inv_id : f⁻¹ * f = 𝟙 x
hom_inv_id₁ : Eq.{u + 1} (α := x ⟶ x) 1 (𝟙 x)
hom_inv_id₂ hom_inv_id₃ : Eq.{u + 1} (α := x ⟶ x) 1 1
⊢ Eq.{u + 1} (α := x ⟶ x) (f ≫ f⁻¹) (𝟙 x)

Tactic:
rw [comp_as_mul, inv_mul_cancel, id_as_one]

Premises used: CategoryTheory.SingleObj.id_as_one, inv_mul_cancel, CategoryTheory.SingleObj.comp_as_mul
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
x : M
⊢ (toEnd M : (a : M) → End (star M)) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
⊢ Eq (α := SingleObj M ⥤ SingleObj M)
    ((mapHom M M : (a : M →* M) → SingleObj M ⥤ SingleObj M) (MonoidHom.id M) : SingleObj M ⥤ SingleObj M)
    (𝟭 (SingleObj M) : SingleObj M ⥤ SingleObj M)

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
N : Type v
inst_1 : Monoid N
f : M →* N
P : Type w
inst_2 : Monoid P
g : N →* P
⊢ Eq (α := Functor.{u, w, 0, 0} (SingleObj M) (SingleObj P))
    ((mapHom M P : (a : M →* P) → SingleObj M ⥤ SingleObj P) (g.comp f) :
      Functor.{u, w, 0, 0} (SingleObj M) (SingleObj P))
    (Functor.comp.{u, v, w, 0, 0, 0} (D := SingleObj N) ((mapHom M N : (a : M →* N) → SingleObj M ⥤ SingleObj N) f)
        ((mapHom N P : (a : N →* P) → SingleObj N ⥤ SingleObj P) g) :
      Functor.{u, w, 0, 0} (SingleObj M) (SingleObj P))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X : C
⊢ f X * (f X)⁻¹ = 𝟙 ()

Tactic:
simp only [SingleObj.id_as_one, mul_inv_cancel]

Premises used: CategoryTheory.SingleObj.id_as_one, mul_inv_cancel
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X Y Z : C
f_1 : X ⟶ Y
g : Y ⟶ Z
rw : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * (f Y * (f X)⁻¹)
rw₁ : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * f Y * (f X)⁻¹
rw₂ : f Z = f Z * (f Y)⁻¹ * f Y
rw₃ : f Z = f Z * ((f Y)⁻¹ * f Y)
rw₄ : f Z = f Z * 1
rw₅ rw₆ : f Z = f Z
⊢ f Z * (f X)⁻¹ = CategoryStruct.comp (Y := ()) (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)

Tactic:
rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]

Premises used: inv_mul_cancel, mul_assoc, mul_left_inj, CategoryTheory.SingleObj.comp_as_mul, mul_one
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
P : Type w
inst_2 : Monoid P
g : N →* P
⊢ (g.comp f).toFunctor = f.toFunctor ⋙ g.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
⊢ Eq (α := SingleObj M ⥤ SingleObj M) (toFunctor (id M)) (𝟭 (SingleObj M))

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
rw : MonoidHom.toFunctor (MonoidHom.id M) = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor
⊢ 𝟭 (SingleObj M) = e.toMonoidHom.toFunctor ⋙ e.symm.toMonoidHom.toFunctor

Tactic:
rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]

Premises used: MonoidHom.id_toFunctor, MonoidHom.comp_toFunctor
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
e_f : MonoidHom.id M = e.symm.toMonoidHom.comp e.toMonoidHom
⊢ MonoidHom.toFunctor (MonoidHom.id M) = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
⊢ MonoidHom.id M = e.symm.toMonoidHom.comp e.toMonoidHom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
rw : (e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = MonoidHom.toFunctor (MonoidHom.id N)
⊢ e.symm.toMonoidHom.toFunctor ⋙ e.toMonoidHom.toFunctor = 𝟭 (SingleObj N)

Tactic:
rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]

Premises used: MonoidHom.id_toFunctor, MonoidHom.comp_toFunctor
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
e_f : e.toMonoidHom.comp e.symm.toMonoidHom = MonoidHom.id N
⊢ (e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = MonoidHom.toFunctor (MonoidHom.id N)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
⊢ e.toMonoidHom.comp e.symm.toMonoidHom = MonoidHom.id N

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
x : Mˣ
⊢ Eq.{u + 1} (α := SingleObj.star M ⟶ SingleObj.star M) (Iso.hom ((toAut M : (a : Mˣ) → Aut (SingleObj.star M)) x))
    ((SingleObj.toEnd M : (a : M) → End (SingleObj.star M)) (↑x : M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
M : Type u
inst : Monoid M
x : Mˣ
⊢ Eq.{u + 1} (α := SingleObj.star M ⟶ SingleObj.star M) (Iso.inv ((toAut M : (a : Mˣ) → Aut (SingleObj.star M)) x))
    ((SingleObj.toEnd M : (a : M) → End (SingleObj.star M)) (↑x⁻¹ : M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SingleObj
Goal:
X Y : MonCat
a₁ a₂ : X ⟶ Y
h : toCat.map a₁ = toCat.map a₂
⊢ Hom.hom a₁ = Hom.hom a₂

Tactic:
simpa [toCat] using congr(($h).toFunctor)

Premises used: MonCat.toCat
-- Module: Mathlib.CategoryTheory.Sites.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : Abelian.{w', w} D
J : GrothendieckTopology.{v, u} C
inst_3 : HasSheafify.{v, w', u, w} J D
⊢ Functor.Additive (C := Functor.{v, w', u, w} Cᵒᵖ D) (presheafToSheaf J D)

Tactic:
(presheafToSheaf J D).additive_of_preservesBinaryBiproducts

Premises used: CategoryTheory.presheafToSheaf, CategoryTheory.Functor.additive_of_preservesBinaryBiproducts