awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o (Subobject.{v, u} X)ᵒᵈ),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
            ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
G : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ
⊢ IsFiltered.IsEventuallyConstant G
have refine_1 : ∀ (n : ℕ)
  (hn :
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ)
          (({
                  toFun :=
                    (G ⋙
                        Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                          Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                  monotone' := sorry : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
                (a : ℕ) → (Subobject X)ᵒᵈ)
              n :
            (Subobject.{v, u} X)ᵒᵈ)
          (({
                  toFun :=
                    (G ⋙
                        Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                          Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                  monotone' := sorry : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
                (a : ℕ) → (Subobject X)ᵒᵈ)
              m :
            (Subobject.{v, u} X)ᵒᵈ)),
  IsFiltered.IsEventuallyConstant G
Tactic: obtain ⟨n, hn⟩ := h ⟨_, (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙
      (orderDualEquivalence _).inverse).monotone⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o (Subobject.{v, u} X)ᵒᵈ),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
            ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
G : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            n :
          (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            m :
          (Subobject.{v, u} X)ᵒᵈ)
⊢ IsFiltered.IsEventuallyConstant G
have refine_1 : ∀ (m : ℕ) (hm : n ⟶ m), IsIso (G.map hm)
Tactic: refine ⟨n, fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o (Subobject.{v, u} X)ᵒᵈ),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
            ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
G : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            n :
          (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            m :
          (Subobject.{v, u} X)ᵒᵈ)
m : ℕ
hm : n ⟶ m
⊢ IsIso (G.map hm)
have refine_1 : Subobject.mk (Opposite.unop (G.obj m)).obj (P := Over.isMono X).hom =
  Subobject.mk (Opposite.unop (G.obj n)).obj (P := Over.isMono X).hom
Tactic: rw [← isIso_unop_iff, MonoOver.isIso_iff_subobjectMk_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject.{v, u} X)ᵒᵈ
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((F : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
          ((F : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
have refine_2 : ∀ (n : ℕ)
  (hn :
    (sorry.functor ⋙
          Equivalence.functor (orderDualEquivalence (Subobject.{v, u} X)) ⋙
            Functor.op Subobject.representative).IsEventuallyConstantFrom
      n),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((F : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
          ((F : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
Tactic: obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ (orderDualEquivalence _).functor ⋙
      Subobject.representative.op)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject.{v, u} X)ᵒᵈ
n : ℕ
hn :
  (⋯.functor ⋙
        Equivalence.functor (orderDualEquivalence (Subobject.{v, u} X)) ⋙
          Functor.op Subobject.representative).IsEventuallyConstantFrom
    n
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((F : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
          ((F : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
have refine_2 : ∀ (m : ℕ) (hm : n ≤ m),
  Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((F : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
    ((F : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
Tactic: refine ⟨n, fun m hm ↦ Eq.symm ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
⊢ IsArtinianObject.{v, u} X
have rw : ∀ (f : ℕ →o (Subobject.{v, u} X)ᵒᵈ),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
          ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
Tactic: rw [isArtinianObject_iff_antitone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
⊢ ∀ (f : ℕ →o (Subobject.{v, u} X)ᵒᵈ),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
            ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
have this : Subsingleton (Subobject.{v, u} X)
Tactic: have := Subobject.subsingleton_of_isZero hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroObject.{v, u} C
⊢ isArtinianObject.{v, u} (C := C) 0
have rw : ObjectProperty.Is.{v, u} (C := C) isArtinianObject 0
Tactic: rw [← isArtinianObject.is_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsArtinianObject.{v, u} Y
⊢ IsArtinianObject.{v, u} X
have rw : ∀ (f : ℕ →o (Subobject.{v, u} X)ᵒᵈ),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
          ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
Tactic: rw [isArtinianObject_iff_antitone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsArtinianObject.{v, u} Y
f : ℕ →o (Subobject.{v, u} X)ᵒᵈ
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
          ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
have obtain : ∀ (n : ℕ)
  (hn :
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} Y)ᵒᵈ)
          (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := sorry } :
                (a : ℕ) → (Subobject Y)ᵒᵈ)
              n :
            (Subobject.{v, u} Y)ᵒᵈ)
          (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := sorry } :
                (a : ℕ) → (Subobject Y)ᵒᵈ)
              m :
            (Subobject.{v, u} Y)ᵒᵈ)),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)
          ((f : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
Tactic: obtain ⟨n, hn⟩ := antitone_chain_condition_of_isArtinianObject
    ⟨fun n ↦ (Subobject.map i).obj (f n),
      fun _ _ h ↦ (Subobject.map i).monotone (f.2 h)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
hY : isArtinianObject.{v, u} Y_1
⊢ isArtinianObject.{v, u} X_1
have rw : ∀ (hY : ObjectProperty.Is.{v, u} isArtinianObject Y_1), ObjectProperty.Is.{v, u} isArtinianObject X_1
Tactic: rw [← isArtinianObject.is_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (hypothesis)
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
⊢ ∃ (Y : Subobject.{v, u} X), Simple.{v, u} (Functor.obj underlying Y)
have this : Nontrivial (Subobject.{v, u} X)
Tactic: have : Nontrivial (Subobject X) := nontrivial_of_not_isZero h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
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), Simple.{v, u} (Functor.obj underlying Y)
have obtain : ∀ (Y : Subobject.{v, u} X) (s : IsAtom Y ∧ Y ≤ ⊤), ∃ (Y : Subobject.{v, u} X), Simple.{v, u} (Functor.obj underlying Y)
Tactic: obtain ⟨Y, s⟩ := (IsAtomic.eq_bot_or_exists_atom_le (⊤ : Subobject X)).resolve_left top_ne_bot
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ p P
have h₁ : ∀ (a : MonoOver.{v₁, u₁} X), p (Quotient.mk'' a)
Tactic: induction P using Quotient.inductionOn' with | _ a
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ p P Q
have h₁ : ∀ (a b : MonoOver.{v₁, u₁} X), p (Quotient.mk'' a) (Quotient.mk'' b)
Tactic: induction P, Q using Quotient.inductionOn₂' with | _ a b
Cleared hypotheses: P, Q
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
X Y : Subobject.{v₁, u₁} A
h : X = Y
⊢ eqToHom ⋯ ≫ Y.arrow = X.arrow
have refl : eqToHom sorry ≫ X.arrow = X.arrow
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
Q : MonoOver.{v₁, u₁} X
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
have obtain : ∀ (e : Quotient.out (s := isIsomorphicSetoid (MonoOver.{v₁, u₁} X)) (Quotient.mk'' Q) ≅ Q),
  mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
Tactic: obtain ⟨e⟩ := @Quotient.mk_out' _ (isIsomorphicSetoid _) Q
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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 ≤ Y
have h : X = mk X.arrow
Tactic: convert! mk_le_mk_of_comm _ w
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ X ≤ Y
have h₁ : Y = mk Y.arrow
Tactic: convert! mk_le_mk_of_comm _ w
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ i.symm.hom ≫ f = X.arrow
have rw : i.inv ≫ f = X.arrow
Tactic: rw [Iso.symm_hom, Iso.inv_comp_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ i.symm.hom ≫ f = X.arrow
have rw₁ : f = i.hom ≫ X.arrow
Tactic: rw [Iso.symm_hom, Iso.inv_comp_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ i.symm.hom ≫ f = X.arrow
have rw₂ : f = f
Tactic: rw [Iso.symm_hom, Iso.inv_comp_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ Mono (X.ofLE Y h)
have 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
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (hypothesis)
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 = g
have w₁ : (f ≫ X.ofLE Y h) ≫ Y.arrow = (g ≫ X.ofLE Y h) ≫ Y.arrow
Tactic: replace w := w =≫ Y.arrow
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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 = g
have right_cancellation : f ≫ X.arrow = g ≫ X.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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₁
⊢ 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₂))
have h : (mk f₁).ofLE (mk f₂) sorry ≫ (mk f₂).arrow = (Iso.hom (underlyingIso f₁) ≫ g ≫ Iso.inv (underlyingIso f₂)) ≫ (mk f₂).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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.ofLEMk f h)
have dsimp : Mono (X.ofLE (mk f) h ≫ Iso.hom (underlyingIso f))
Tactic: dsimp only [ofLEMk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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 (ofMkLE f X h)
have dsimp : Mono (Iso.inv (underlyingIso f) ≫ (mk f).ofLE X h)
Tactic: dsimp only [ofMkLE]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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 (ofMkLEMk f g h)
have dsimp : Mono (Iso.inv (underlyingIso f) ≫ (mk f).ofLE (mk g) h ≫ Iso.hom (underlyingIso g))
Tactic: dsimp only [ofMkLEMk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X Y Z : Subobject.{v₁, u₁} B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ X.ofLE Y h₁ ≫ Y.ofLE Z h₂ = X.ofLE Z ⋯
have simp : Eq (α := Functor.obj underlying X ⟶ Functor.obj underlying Z) (Functor.map underlying (h₁.hom ≫ h₂.hom))
  (Functor.map underlying sorry.hom)
Tactic: simp only [ofLE, ← Functor.map_comp underlying]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ X.ofLE Y h₁ ≫ Y.ofLEMk f h₂ = X.ofLEMk f ⋯
have simp : Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso f) =
  Functor.map underlying sorry.hom ≫ Iso.hom (underlyingIso f)
Tactic: simp only [ofLEMk, ofLE, ← Functor.map_comp_assoc underlying]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ X.ofLEMk f h₁ ≫ ofMkLE f Y h₂ = X.ofLE Y ⋯
have simp : Eq (α := Functor.obj underlying X ⟶ Functor.obj underlying Y) (Functor.map underlying (h₁.hom ≫ h₂.hom))
  (Functor.map underlying sorry.hom)
Tactic: simp only [ofMkLE, ofLEMk, ofLE, ← Functor.map_comp underlying, assoc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ X.ofLEMk f h₁ ≫ ofMkLEMk f g h₂ = X.ofLEMk g ⋯
have simp : Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso g) =
  Functor.map underlying sorry.hom ≫ Iso.hom (underlyingIso g)
Tactic: simp only [ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying,
    assoc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ ofMkLE f X h₁ ≫ X.ofLE Y h₂ = ofMkLE f Y ⋯
have simp : Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) =
  Iso.inv (underlyingIso f) ≫ Functor.map underlying sorry.hom
Tactic: simp only [ofMkLE, ofLE, ← Functor.map_comp underlying,
    assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
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
⊢ ofMkLE f X h₁ ≫ X.ofLEMk g h₂ = ofMkLEMk f g ⋯
have simp : Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso g) =
  Iso.inv (underlyingIso f) ≫ Functor.map underlying sorry.hom ≫ Iso.hom (underlyingIso g)
Tactic: simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
X : Subobject.{v₁, u₁} B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X ⋯
have simp : Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) =
  Iso.inv (underlyingIso f) ≫ Functor.map underlying sorry.hom
Tactic: simp only [ofMkLE, ofLE, ofMkLEMk, ← Functor.map_comp underlying,
    assoc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
h : A₃ ⟶ B
inst_3 : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
⊢ ofMkLEMk f g h₁ ≫ ofMkLEMk g h h₂ = ofMkLEMk f h ⋯
have simp : Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso h) =
  Iso.inv (underlyingIso f) ≫ Functor.map underlying sorry.hom ≫ Iso.hom (underlyingIso h)
Tactic: simp only [ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc,
    Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X : Subobject.{v₁, u₁} B
⊢ X.ofLE X ⋯ = 𝟙 (Functor.obj underlying X)
have apply : X.ofLE X sorry ≫ X.arrow = 𝟙 (Functor.obj underlying X) ≫ X.arrow
Tactic: apply (cancel_mono X.arrow).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst_1 : Mono f
⊢ ofMkLEMk f f ⋯ = 𝟙 A₁
have apply : ofMkLEMk f f sorry ≫ f = 𝟙 A₁ ≫ f
Tactic: apply (cancel_mono f).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
⊢ mk i₁ < mk i₂
have inl : mk i₁ < mk i₂ → mk i₁ < mk i₂
Tactic: obtain _ | h := (mk_le_mk_of_comm _ fac).lt_or_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
inl : mk i₁ < mk i₂ → mk i₁ < mk i₂
⊢ mk i₁ < mk i₂
have inr : ∀ (h : mk i₁ = mk i₂), mk i₁ < mk i₂
Tactic: obtain _ | h := (mk_le_mk_of_comm _ fac).lt_or_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ mk i₁ < mk i₂
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ False
have inr : IsIso f
Tactic: apply hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ IsIso f
have h₁ : f = (isoOfMkEqMk i₁ i₂ h).hom
Tactic: convert! (isoOfMkEqMk i₁ i₂ h).isIso_hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ f = (isoOfMkEqMk i₁ i₂ h).hom
have h₁ : f ≫ i₂ = (isoOfMkEqMk i₁ i₂ h).hom ≫ i₂
Tactic: rw [← cancel_mono i₂, isoOfMkEqMk_hom, ofMkLEMk_comp, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
h₁ : f ≫ i₂ = (isoOfMkEqMk i₁ i₂ h).hom ≫ i₂
⊢ f = (isoOfMkEqMk i₁ i₂ h).hom
have h₂ : f ≫ i₂ = ofMkLEMk i₁ i₂ sorry ≫ i₂
Tactic: rw [← cancel_mono i₂, isoOfMkEqMk_hom, ofMkLEMk_comp, fac]