awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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 : IsArtinianObject.{v, u} X
h : ¬IsZero.{v, u} X
this : Nontrivial (Subobject.{v, u} X)
Y : Subobject.{v, u} X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ (Y : Subobject.{v, u} X), Simple.{v, u} (Functor.obj underlying Y)

Tactic:
exact ⟨Y, (subobject_simple_iff_isAtom _).mpr s.1⟩
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsArtinianObject.{v, u} X
h : ¬IsZero.{v, u} X
⊢ Mono (Exists.choose (p := fun (Y : Subobject.{v, u} X) ↦ Simple.{v, u} (Functor.obj underlying Y)) ⋯).arrow

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsArtinianObject.{v, u} X
h : ¬IsZero.{v, u} X
⊢ Simple.{v, u} (simpleSubobject h)

Tactic:
(exists_simple_subobject h).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.exists_simple_subobject, CategoryTheory.simpleSubobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Skeletal (Subobject.{v₁, u₁} X)

Tactic:
ThinSkeleton.skeletal

Premises used: CategoryTheory.ThinSkeleton, CategoryTheory.ThinSkeleton.skeletal, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
p : Subobject.{v₁, u₁} X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst_1 : Mono f], p (mk f)
P : Subobject.{v₁, u₁} X
h₁ : ∀ (a : MonoOver.{v₁, u₁} X), p (Quotient.mk'' a)
⊢ p P

Tactic:
induction P using Quotient.inductionOn' with | _ a
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
p : Subobject.{v₁, u₁} X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst_1 : Mono f], p (mk f)
a : MonoOver.{v₁, u₁} X
⊢ p (Quotient.mk'' a)

Tactic:
h a.arrow

Premises used: CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.MonoOver.mk, CategoryTheory.CostructuredArrow, CategoryTheory.Subobject.mk, Quotient.mk', CategoryTheory.CostructuredArrow.mk, CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
p : Subobject.{v₁, u₁} X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst_1 : Mono f], p (mk f)
a : MonoOver.{v₁, u₁} X
⊢ p (Quotient.mk'' a)

Tactic:
exact h a.arrow

Premises used: CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
p : Subobject.{v₁, u₁} X → Subobject.{v₁, u₁} X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_1 : Mono f] [inst_2 : Mono g], p (mk f) (mk g)
P Q : Subobject.{v₁, u₁} X
h₁ : ∀ (a b : MonoOver.{v₁, u₁} X), p (Quotient.mk'' a) (Quotient.mk'' b)
⊢ p P Q

Tactic:
induction P, Q using Quotient.inductionOn₂' with | _ a b
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
p : Subobject.{v₁, u₁} X → Subobject.{v₁, u₁} X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_1 : Mono f] [inst_2 : Mono g], p (mk f) (mk g)
a b : MonoOver.{v₁, u₁} X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)

Tactic:
h a.arrow b.arrow

Premises used: CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.MonoOver.mk, CategoryTheory.CostructuredArrow, CategoryTheory.Subobject.mk, Quotient.mk', CategoryTheory.CostructuredArrow.mk, CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
p : Subobject.{v₁, u₁} X → Subobject.{v₁, u₁} X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_1 : Mono f] [inst_2 : Mono g], p (mk f) (mk g)
a b : MonoOver.{v₁, u₁} X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)

Tactic:
exact h a.arrow b.arrow

Premises used: CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Sort u_1
X : C
F : ⦃A : C⦄ → (f : A ⟶ X) → [Mono f] → α
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_2 : Mono f] [inst_3 : Mono g] (i : A ≅ B), i.hom ≫ g = f → F f = F g
A : C
f : A ⟶ X
inst_1 : Mono f
⊢ Subobject.lift F h (mk f) = F f

Tactic:
rfl

Premises used: Quotient.liftOn', CategoryTheory.Subobject.lift, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ Functor.IsEquivalence (C := Subobject.{v₁, u₁} X) representative

Tactic:
(equivMonoOver X).isEquivalence_functor

Premises used: CategoryTheory.Subobject.equivMonoOver, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Subobject.representative
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
A : Subobject.{v₁, u₁} X
⊢ ThinSkeleton.mk (Functor.obj representative A) = A

Tactic:
Subobject.skeletal _ ⟨((equivMonoOver X).unitIso.app _).symm⟩

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Subobject.equivMonoOver, Nonempty.intro, CategoryTheory.Subobject.skeletal, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
Y : Subobject.{v₁, u₁} X
⊢ Mono Y.arrow

Tactic:
(representative.obj Y).property

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Subobject.representative, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
X Y : Subobject.{v₁, u₁} A
h : X = Y
refl : eqToHom ⋯ ≫ X.arrow = X.arrow
⊢ eqToHom ⋯ ≫ Y.arrow = X.arrow

Tactic:
induction h
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
X Y : Subobject.{v₁, u₁} A
⊢ eqToHom ⋯ ≫ X.arrow = X.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y : Subobject.{v₁, u₁} X
⊢ (Functor.obj representative Y).obj (P := Over.isMono X).left = Functor.obj underlying Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y : Subobject.{v₁, u₁} X
⊢ (Functor.obj representative Y).arrow = Y.arrow

Tactic:
rfl

Premises used: CategoryTheory.Subobject.arrow, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y Z : Subobject.{v₁, u₁} X
f : Y ⟶ Z
⊢ Functor.map underlying f ≫ Z.arrow = Y.arrow

Tactic:
Over.w (representative.map f).hom

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Functor.map, CategoryTheory.Over.w, CategoryTheory.Subobject.representative, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Iso.inv (underlyingIso f) ≫ (mk f).arrow = f

Tactic:
Over.w _

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Over.w, CategoryTheory.Subobject.mk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Iso.hom (underlyingIso f) ≫ f = (mk f).arrow

Tactic:
(Iso.eq_inv_comp _).1 (underlyingIso_arrow f).symm

Premises used: CategoryTheory.Subobject.underlyingIso_arrow, Iff.mp, CategoryTheory.Iso.eq_inv_comp, Eq.symm
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Functor.obj underlying P
h : f ≫ P.arrow = g ≫ P.arrow
⊢ f = g

Tactic:
(cancel_mono P.arrow).mp h

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst_1 : Mono f₁
inst_2 : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
⊢ mk f₁ ≤ mk f₂

Tactic:
⟨MonoOver.homMk _ w⟩

Premises used: Nonempty.intro, CategoryTheory.MonoOver.homMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
Q : MonoOver.{v₁, u₁} X
obtain :
  ∀ (e : Quotient.out (s := isIsomorphicSetoid (MonoOver.{v₁, u₁} X)) (Quotient.mk'' Q) ≅ Q),
    mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q

Tactic:
obtain ⟨e⟩ := @Quotient.mk_out' _ (isIsomorphicSetoid _) Q

Premises used: Quotient.mk_out'
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
Q : MonoOver.{v₁, u₁} X
e : Quotient.out (s := isIsomorphicSetoid (MonoOver.{v₁, u₁} X)) (Quotient.mk'' Q) ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q

Tactic:
Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _) ≪≫ e⟩

Premises used: Quotient.sound', CategoryTheory.Iso.refl, Nonempty.intro, CategoryTheory.ThinSkeleton, CategoryTheory.MonoOver.isoMk, CategoryTheory.Subobject.mk, Quotient.mk', CategoryTheory.Iso.trans, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
Q : MonoOver.{v₁, u₁} X
e : Quotient.out (s := isIsomorphicSetoid (MonoOver.{v₁, u₁} X)) (Quotient.mk'' Q) ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q

Tactic:
exact Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _) ≪≫ e⟩
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
f : Functor.obj underlying X ⟶ Functor.obj underlying Y
w : f ≫ Y.arrow = X.arrow
⊢ mk X.arrow ≤ mk Y.arrow

Tactic:
mk_le_mk_of_comm _ w

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
f : Functor.obj underlying X ⟶ Functor.obj underlying Y
w : f ≫ Y.arrow = X.arrow
h : X = mk X.arrow
h₁ : Y = mk Y.arrow
⊢ X ≤ Y

Tactic:
convert! mk_le_mk_of_comm _ w

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
f : Functor.obj underlying X ⟶ Functor.obj underlying Y
w : f ≫ Y.arrow = X.arrow
⊢ X = mk X.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
f : Functor.obj underlying X ⟶ Functor.obj underlying Y
w : f ≫ Y.arrow = X.arrow
⊢ Y = mk Y.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
g : Functor.obj underlying X ⟶ A
w : g ≫ f = X.arrow
⊢ (g ≫ Iso.inv (underlyingIso f)) ≫ (mk f).arrow = X.arrow

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
g : A ⟶ Functor.obj underlying X
w : g ≫ X.arrow = f
⊢ (Iso.hom (underlyingIso f) ≫ g) ≫ X.arrow = (mk f).arrow

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
f : Functor.obj underlying X ≅ Functor.obj underlying Y
w : f.hom ≫ Y.arrow = X.arrow
⊢ X = Y

Tactic:
le_antisymm (le_of_comm f.hom w) <| le_of_comm f.inv <| f.inv_comp_eq.2 w.symm

Premises used: Iff.mpr, CategoryTheory.Subobject.le_of_comm, CategoryTheory.Iso.inv_comp_eq, le_antisymm, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
i : Functor.obj underlying X ≅ A
w : i.hom ≫ f = X.arrow
⊢ Iso.hom (i ≪≫ Iso.symm (underlyingIso f)) ≫ (mk f).arrow = X.arrow

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
i : A ≅ Functor.obj underlying X
w : i.hom ≫ X.arrow = f
rw : i.inv ≫ f = X.arrow
rw₁ : f = i.hom ≫ X.arrow
rw₂ rw₃ : f = f
⊢ i.symm.hom ≫ f = X.arrow

Tactic:
rw [Iso.symm_hom, Iso.inv_comp_eq, w]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Iso.symm_hom
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst_1 : Mono f
inst_2 : Mono g
i : A₁ ≅ A₂
w : i.hom ≫ g = f
⊢ Iso.hom (underlyingIso f ≪≫ i) ≫ g = (mk f).arrow

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Subobject.{v₁, u₁} X
⊢ S = mk S.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
h : X ≤ Y
⊢ X.ofLE Y h ≫ Y.arrow = X.arrow

Tactic:
underlying_arrow _

Premises used: CategoryTheory.Subobject.ofLE, CategoryTheory.Subobject.underlying_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B : C
X Y : Subobject.{v₁, u₁} B
h : X ≤ Y
right_cancellation : ∀ {Z : C} (g h_1 : Z ⟶ Functor.obj underlying X), g ≫ X.ofLE Y h = h_1 ≫ X.ofLE Y h → g = h_1
⊢ Mono (X.ofLE Y h)

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B : C
X Y : Subobject.{v₁, u₁} B
h : X ≤ Y
Z : C
f g : Z ⟶ Functor.obj underlying X
w : f ≫ X.ofLE Y h = g ≫ X.ofLE Y h
⊢ (f ≫ X.ofLE Y h) ≫ Y.arrow = (g ≫ X.ofLE Y h) ≫ Y.arrow

Tactic:
replace w := w =≫ Y.arrow
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B : C
X Y : Subobject.{v₁, u₁} B
h : X ≤ Y
Z : C
f g : Z ⟶ Functor.obj underlying X
w : (f ≫ X.ofLE Y h) ≫ Y.arrow = (g ≫ X.ofLE Y h) ≫ Y.arrow
right_cancellation : f ≫ X.arrow = g ≫ X.arrow
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B : C
X Y : Subobject.{v₁, u₁} B
h : X ≤ Y
Z : C
f g : Z ⟶ Functor.obj underlying X
w : (f ≫ X.ofLE Y h) ≫ Y.arrow = (g ≫ X.ofLE Y h) ≫ Y.arrow
⊢ f ≫ X.arrow = g ≫ X.arrow

Tactic:
simpa using w
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst_1 : Mono f₁
inst_2 : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
h :
  (mk f₁).ofLE (mk f₂) ⋯ ≫ (mk f₂).arrow = (Iso.hom (underlyingIso f₁) ≫ g ≫ Iso.inv (underlyingIso f₂)) ≫ (mk f₂).arrow
⊢ Eq (α := Functor.obj underlying (mk f₁) ⟶ Functor.obj underlying (mk f₂)) ((mk f₁).ofLE (mk f₂) ⋯)
    (Iso.hom (underlyingIso f₁) ≫ g ≫ Iso.inv (underlyingIso f₂))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst_1 : Mono f₁
inst_2 : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
⊢ (mk f₁).ofLE (mk f₂) ⋯ ≫ (mk f₂).arrow = (Iso.hom (underlyingIso f₁) ≫ g ≫ Iso.inv (underlyingIso f₂)) ≫ (mk f₂).arrow

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_2 : Mono f
h : X ≤ mk f
dsimp : Mono (X.ofLE (mk f) h ≫ Iso.hom (underlyingIso f))
⊢ Mono (X.ofLEMk f h)

Tactic:
dsimp only [ofLEMk]

Premises used: CategoryTheory.Subobject.ofLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_2 : Mono f
h : X ≤ mk f
⊢ Mono (X.ofLE (mk f) h ≫ Iso.hom (underlyingIso f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
h : X ≤ mk f
⊢ X.ofLEMk f h ≫ f = X.arrow

Tactic:
simp [ofLEMk]

Premises used: CategoryTheory.Subobject.ofLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst_2 : Mono f
X : Subobject.{v₁, u₁} B
h : mk f ≤ X
dsimp : Mono (Iso.inv (underlyingIso f) ≫ (mk f).ofLE X h)
⊢ Mono (ofMkLE f X h)

Tactic:
dsimp only [ofMkLE]

Premises used: CategoryTheory.Subobject.ofMkLE
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst_2 : Mono f
X : Subobject.{v₁, u₁} B
h : mk f ≤ X
⊢ Mono (Iso.inv (underlyingIso f) ≫ (mk f).ofLE X h)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
f : A ⟶ B
inst_1 : Mono f
X : Subobject.{v₁, u₁} B
h : mk f ≤ X
⊢ ofMkLE f X h ≫ X.arrow = f

Tactic:
simp [ofMkLE]

Premises used: CategoryTheory.Subobject.ofMkLE
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst_2 : Mono f
inst_3 : Mono g
h : mk f ≤ mk g
dsimp : Mono (Iso.inv (underlyingIso f) ≫ (mk f).ofLE (mk g) h ≫ Iso.hom (underlyingIso g))
⊢ Mono (ofMkLEMk f g h)

Tactic:
dsimp only [ofMkLEMk]

Premises used: CategoryTheory.Subobject.ofMkLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst_2 : Mono f
inst_3 : Mono g
h : mk f ≤ mk g
⊢ Mono (Iso.inv (underlyingIso f) ≫ (mk f).ofLE (mk g) h ≫ Iso.hom (underlyingIso g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst_1 : Mono f
inst_2 : Mono g
h : mk f ≤ mk g
⊢ ofMkLEMk f g h ≫ g = f

Tactic:
simp [ofMkLEMk]

Premises used: CategoryTheory.Subobject.ofMkLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y Z : Subobject.{v₁, u₁} B
h₁ : X ≤ Y
h₂ : Y ≤ Z
simp :
  Eq (α := Functor.obj underlying X ⟶ Functor.obj underlying Z) (Functor.map underlying (h₁.hom ≫ h₂.hom))
    (Functor.map underlying ⋯.hom)
⊢ X.ofLE Y h₁ ≫ Y.ofLE Z h₂ = X.ofLE Z ⋯

Tactic:
simp only [ofLE, ← Functor.map_comp underlying]

Premises used: CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y Z : Subobject.{v₁, u₁} B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ Eq (α := Functor.obj underlying X ⟶ Functor.obj underlying Z) (Functor.map underlying (h₁.hom ≫ h₂.hom))
    (Functor.map underlying ⋯.hom)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X Y : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
simp :
  Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso f) =
    Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso f)
⊢ X.ofLE Y h₁ ≫ Y.ofLEMk f h₂ = X.ofLEMk f ⋯

Tactic:
simp only [ofLEMk, ofLE, ← Functor.map_comp_assoc underlying]

Premises used: CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Subobject.ofLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X Y : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
⊢ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso f) =
    Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso f)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
Y : Subobject.{v₁, u₁} B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
simp :
  Eq (α := Functor.obj underlying X ⟶ Functor.obj underlying Y) (Functor.map underlying (h₁.hom ≫ h₂.hom))
    (Functor.map underlying ⋯.hom)
⊢ X.ofLEMk f h₁ ≫ ofMkLE f Y h₂ = X.ofLE Y ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ← Functor.map_comp underlying, assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Subobject.ofMkLE, CategoryTheory.Subobject.ofLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A : C
X : Subobject.{v₁, u₁} B
f : A ⟶ B
inst_1 : Mono f
Y : Subobject.{v₁, u₁} B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ Eq (α := Functor.obj underlying X ⟶ Functor.obj underlying Y) (Functor.map underlying (h₁.hom ≫ h₂.hom))
    (Functor.map underlying ⋯.hom)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
X : Subobject.{v₁, u₁} B
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
simp :
  Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso g) =
    Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso g)
⊢ X.ofLEMk f h₁ ≫ ofMkLEMk f g h₂ = X.ofLEMk g ⋯

Tactic:
simp only [ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying,
    assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Subobject.ofMkLEMk, CategoryTheory.Subobject.ofLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
X : Subobject.{v₁, u₁} B
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso g) =
    Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso g)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst_1 : Mono f
X Y : Subobject.{v₁, u₁} B
h₁ : mk f ≤ X
h₂ : X ≤ Y
simp :
  Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom
⊢ ofMkLE f X h₁ ≫ X.ofLE Y h₂ = ofMkLE f Y ⋯

Tactic:
simp only [ofMkLE, ofLE, ← Functor.map_comp underlying,
    assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Functor.map_comp, CategoryTheory.Subobject.ofMkLE
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst_1 : Mono f
X Y : Subobject.{v₁, u₁} B
h₁ : mk f ≤ X
h₂ : X ≤ Y
⊢ Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst_1 : Mono f
X : Subobject.{v₁, u₁} B
g : A₂ ⟶ B
inst_2 : Mono g
h₁ : mk f ≤ X
h₂ : X ≤ mk g
simp :
  Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso g) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso g)
⊢ ofMkLE f X h₁ ≫ X.ofLEMk g h₂ = ofMkLEMk f g ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Subobject.ofMkLEMk, CategoryTheory.Subobject.ofMkLE, CategoryTheory.Subobject.ofLEMk