awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject.{v₁, u₁} Y
f : Z ⟶ Y
h : P ≤ Q
⊢ P.Factors f → Q.Factors f
have simp : (Functor.obj representative P).Factors f → (Functor.obj representative Q).Factors f
Tactic: simp only [factors_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
h : P.Factors P.arrow
⊢ P.factorThru P.arrow h = 𝟙 (Functor.obj underlying P)
have h₁ : P.factorThru P.arrow h ≫ P.arrow = 𝟙 (Functor.obj underlying P) ≫ P.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ (mk f).factorThru f ⋯ = Iso.inv (underlyingIso f)
have h : (mk f).factorThru f sorry ≫ (mk f).arrow = Iso.inv (underlyingIso f) ≫ (mk f).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Functor.obj underlying P
h : P.Factors (f ≫ P.arrow)
⊢ P.factorThru (f ≫ P.arrow) h = f
have h₁ : P.factorThru (f ≫ P.arrow) h ≫ P.arrow = f ≫ P.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
h : P.Factors f
⊢ P.factorThru f h = 0 ↔ f = 0
have mp : P.factorThru f h = 0 → f = 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
h : P.Factors f
mp : P.factorThru f h = 0 → f = 0
⊢ P.factorThru f h = 0 ↔ f = 0
have mpr : f = 0 → P.factorThru f h = 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h = 0
⊢ f = 0
have w₁ : P.factorThru f h ≫ P.arrow = 0 ≫ P.arrow
Tactic: replace w := w =≫ P.arrow
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
h : P.Factors (X := X) 0
⊢ P.factorThru 0 h = 0
have mpr : P.factorThru 0 h ≫ P.arrow = 0 ≫ P.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
P : Subobject.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ f ≫ P.factorThru g h = P.factorThru (f ≫ g) ⋯
have apply : (f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) sorry ≫ P.arrow
Tactic: apply (cancel_mono P.arrow).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject.{v₁, u₁} Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
⊢ Q.factorThru f ⋯ = P.factorThru f w ≫ P.ofLE Q h
have h₁ : Q.factorThru f sorry ≫ Q.arrow = (P.factorThru f w ≫ P.ofLE Q h) ≫ Q.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
⊢ P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg
have h : P.factorThru (f + g) w ≫ P.arrow = (P.factorThru f wf + P.factorThru g wg) ≫ P.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f ⋯
have h : (P.factorThru (f + g) w - P.factorThru g wg) ≫ P.arrow = P.factorThru f sorry ≫ P.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g ⋯
have h : (P.factorThru (f + g) w - P.factorThru f wf) ≫ P.arrow = P.factorThru g sorry ≫ P.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B) (initial.to B) 0
have rw : Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B)
  (arrow ⊥ : Over.left.{v₁, u₁} (X := B) (ObjectProperty.FullSubcategory.obj (P := Over.isMono B) ⊥) ⟶ B) 0
Tactic: rw [← bot_arrow, bot_arrow_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
B : C
rw :
  Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B)
    (arrow ⊥ : Over.left.{v₁, u₁} (X := B) (ObjectProperty.FullSubcategory.obj (P := Over.isMono B) ⊥) ⟶ B) 0
⊢ Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B) (initial.to B) 0
have rw₁ : Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B) 0 0
Tactic: rw [← bot_arrow, bot_arrow_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
⊢ (pullback X_1.arrow ⋙ map X_1.arrow).obj g ⟶ (pullback Y_1.arrow ⋙ map Y_1.arrow).obj g
have apply : ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).obj (P := Over.isMono A).left ⟶
  ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).obj (P := Over.isMono A).left
Tactic: apply homMk _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
apply :
  ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).obj (P := Over.isMono A).left ⟶
    ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).obj (P := Over.isMono A).left
⊢ (pullback X_1.arrow ⋙ map X_1.arrow).obj g ⟶ (pullback Y_1.arrow ⋙ map Y_1.arrow).obj g
have apply₁ : pullback.lift (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow)
      (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) sorry ≫
    ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).arrow =
  ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).arrow
Tactic: apply homMk _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
⊢ ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).obj (P := Over.isMono A).left ⟶
    ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).obj (P := Over.isMono A).left
have apply : Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
  (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow ≫ (Functor.obj (forget A) g).hom)
  ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
Tactic: apply pullback.lift (pullback.fst _ _) (pullback.snd _ _ ≫ k.hom.left) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
⊢ Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow ≫ (Functor.obj (forget A) g).hom)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
have rw : Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
  (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
  ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
Tactic: rw [pullback.condition, assoc, w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
rw :
  Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
⊢ Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow ≫ (Functor.obj (forget A) g).hom)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
have rw₁ : Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
  (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
  (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom ≫ Y_1.arrow)
Tactic: rw [pullback.condition, assoc, w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
rw :
  Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
rw₁ :
  Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom ≫ Y_1.arrow)
⊢ Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow ≫ (Functor.obj (forget A) g).hom)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
have rw₂ : Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
  (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
  (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
Tactic: rw [pullback.condition, assoc, w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
⊢ pullback.lift (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow)
        (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯ ≫
      ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).arrow =
    ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).arrow
have dsimp : Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
  (CategoryStruct.comp (Y := Limits.pullback g.arrow Y_1.arrow)
    (pullback.lift (pullback.fst g.obj (P := Over.isMono A).hom X_1.arrow)
      (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) sorry)
    (pullback.snd g.obj (P := Over.isMono A).hom Y_1.arrow ≫ Y_1.arrow))
  (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
⊢ Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    (CategoryStruct.comp (Y := Limits.pullback g.arrow Y_1.arrow)
      (pullback.lift (pullback.fst g.obj (P := Over.isMono A).hom X_1.arrow)
        (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯)
      (pullback.snd g.obj (P := Over.isMono A).hom Y_1.arrow ≫ Y_1.arrow))
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
have rw : Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
  ((pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
  (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
Tactic: rw [pullback.lift_snd_assoc, assoc, w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
rw :
  Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    ((pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
⊢ Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    (CategoryStruct.comp (Y := Limits.pullback g.arrow Y_1.arrow)
      (pullback.lift (pullback.fst g.obj (P := Over.isMono A).hom X_1.arrow)
        (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯)
      (pullback.snd g.obj (P := Over.isMono A).hom Y_1.arrow ≫ Y_1.arrow))
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
have rw₁ : Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
  (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom ≫ Y_1.arrow)
  (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
Tactic: rw [pullback.lift_snd_assoc, assoc, w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
rw :
  Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    ((pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
rw₁ :
  Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom ≫ Y_1.arrow)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
⊢ Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    (CategoryStruct.comp (Y := Limits.pullback g.arrow Y_1.arrow)
      (pullback.lift (pullback.fst g.obj (P := Over.isMono A).hom X_1.arrow)
        (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯)
      (pullback.snd g.obj (P := Over.isMono A).hom Y_1.arrow ≫ Y_1.arrow))
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
have rw₂ : Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A) (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
  (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
Tactic: rw [pullback.lift_snd_assoc, assoc, w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
⊢ f ⟶ (Functor.obj sup f).obj g
have refine : (coprod.inl ≫
      factorThruImage
        (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
            (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
    ((Functor.obj sup f).obj g).arrow =
  f.arrow
Tactic: refine homMk (coprod.inl ≫ factorThruImage _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
⊢ (coprod.inl ≫
        factorThruImage
          (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
              (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
      ((Functor.obj sup f).obj g).arrow =
    f.arrow
have erw : (Functor.obj (Functor.prod (forget A) (forget A)) (f, g)).1.hom = f.arrow
Tactic: erw [Category.assoc, image.fac, coprod.inl_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
⊢ g ⟶ (Functor.obj sup f).obj g
have refine : (coprod.inr ≫
      factorThruImage
        (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
            (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
    ((Functor.obj sup f).obj g).arrow =
  g.arrow
Tactic: refine homMk (coprod.inr ≫ factorThruImage _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
⊢ (coprod.inr ≫
        factorThruImage
          (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
              (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
      ((Functor.obj sup f).obj g).arrow =
    g.arrow
have erw : (Functor.obj (Functor.prod (forget A) (forget A)) (f, g)).2.hom = g.arrow
Tactic: erw [Category.assoc, image.fac, coprod.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ (Functor.obj sup f).obj g ⟶ h
have refine_1 : ((Functor.obj sup f).obj g).obj (P := Over.isMono A).left ⟶ h.obj (P := Over.isMono A).left
Tactic: refine homMk ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
refine_1 : ((Functor.obj sup f).obj g).obj (P := Over.isMono A).left ⟶ h.obj (P := Over.isMono A).left
⊢ (Functor.obj sup f).obj g ⟶ h
have refine_2 : image.lift
      { I := h.obj (P := Over.isMono A).left, m := h.arrow, m_mono := sorry,
        e := coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom), fac := sorry } ≫
    h.arrow =
  ((Functor.obj sup f).obj g).arrow
Tactic: refine homMk ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ((Functor.obj sup f).obj g).obj (P := Over.isMono A).left ⟶ h.obj (P := Over.isMono A).left
have apply : coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
  (Functor.obj (Functor.obj Functor.uncurry Over.coprod) (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
Tactic: apply image.lift ⟨_, h.arrow, coprod.desc k₁.hom.left k₂.hom.left, _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
        (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
have h₁ : CategoryStruct.comp (Y := coprod.{v₁, u₁} f.obj (P := Over.isMono A).left g.obj (P := Over.isMono A).left) coprod.inl
    (coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow) =
  coprod.inl ≫
    (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
        (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
h₁ :
  CategoryStruct.comp (Y := coprod.{v₁, u₁} f.obj (P := Over.isMono A).left g.obj (P := Over.isMono A).left) coprod.inl
      (coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow) =
    coprod.inl ≫
      (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
          (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
⊢ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
        (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
have h₂ : CategoryStruct.comp (Y := coprod.{v₁, u₁} f.obj (P := Over.isMono A).left g.obj (P := Over.isMono A).left) coprod.inr
    (coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow) =
  coprod.inr ≫
    (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
        (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
⊢ ∀ (a : Subobject.{v₁, u₁} X), a ≤ Quotient.mk'' ⊤
have refine : ∀ (f : MonoOver.{v₁, u₁} X), LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' f) (Quotient.mk'' ⊤)
Tactic: refine Quotient.ind' fun f => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := Functor.obj (C := Subobject.{v₁, u₁} B) underlying (mk (𝟙 B)) ⟶ B) (Iso.hom (underlyingIso (𝟙 B)))
    (arrow ⊤)
have h : Eq.{v₁ + 1} (α := Functor.obj (C := Subobject.{v₁, u₁} B) underlying (mk (𝟙 B)) ⟶ B) (Iso.hom (underlyingIso (𝟙 B)))
  (Iso.hom (underlyingIso (𝟙 B)) ≫ 𝟙 B)
Tactic: convert! underlyingIso_hom_comp_eq_mk (𝟙 B)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
B : C
⊢ IsIso.{v₁, u₁} (C := C) (X := Functor.obj (C := Subobject.{v₁, u₁} B) underlying ⊤) (arrow ⊤)
have rw : IsIso.{v₁, u₁} (X := Functor.obj (C := Subobject.{v₁, u₁} B) underlying ⊤) (Iso.hom (underlyingIso (𝟙 B)))
Tactic: rw [← underlyingIso_top_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : mk f = ⊤
⊢ IsIso f
have rw : IsIso (ofMkLEMk f (𝟙 Y) sorry)
Tactic: rw [← ofMkLEMk_comp h.le, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y : C
P : Subobject.{v₁, u₁} Y
⊢ IsIso P.arrow ↔ P = ⊤
have rw : mk P.arrow = ⊤ ↔ P = ⊤
Tactic: rw [isIso_iff_mk_eq_top, mk_arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y : C
P : Subobject.{v₁, u₁} Y
rw : mk P.arrow = ⊤ ↔ P = ⊤
⊢ IsIso P.arrow ↔ P = ⊤
have rw₁ : P = ⊤ ↔ P = ⊤
Tactic: rw [isIso_iff_mk_eq_top, mk_arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
Y : C
⊢ IsIso.{v₁, u₁} (C := C) (X := Functor.obj (C := Subobject.{v₁, u₁} Y) underlying ⊤) (arrow ⊤)
have rw : Eq (α := Subobject.{v₁, u₁} Y) ⊤ ⊤
Tactic: rw [isIso_arrow_iff_eq_top]