awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{v₁, u₁} C
I : Type u_1
A B : C
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
a : I
s : Finset I
h_1 : a ∉ s
ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
j : I
m : j ∈ insert a s
h : (P j).Factors f
⊢ (P a ⊔ s.sup P).Factors f
have m₁ : j = a ∨ j ∈ s
Tactic: simp only [Finset.mem_insert] at m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{v₁, u₁} C
I : Type u_1
A B : C
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
a : I
s : Finset I
h_1 : a ∉ s
ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
j : I
h : (P j).Factors f
m : j = a ∨ j ∈ s
⊢ (P a ⊔ s.sup P).Factors f
have insert : j ∉ s → (P j ⊔ s.sup P).Factors f
Tactic: rcases m with (rfl | m)
Cleared hypotheses: a, h_1, m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{v₁, u₁} C
I : Type u_1
A B : C
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
a : I
s : Finset I
h_1 : a ∉ s
ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
j : I
h : (P j).Factors f
m : j = a ∨ j ∈ s
insert : j ∉ s → (P j ⊔ s.sup P).Factors f
⊢ (P a ⊔ s.sup P).Factors f
have insert₁ : ∀ (m : j ∈ s), (P a ⊔ s.sup P).Factors f
Tactic: rcases m with (rfl | m)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{v₁, u₁} C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
⊢ ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
have empty : ∀ (h : ∃ (i : I), Membership.mem (γ := Finset I) ∅ i ∧ (P i).Factors f), (Finset.sup ∅ P).Factors f
Tactic: induction s using Finset.induction_on with
  | empty => rintro ⟨_, ⟨⟨⟩, _⟩⟩
  | insert _ _ _ ih =>
    rintro ⟨j, ⟨m, h⟩⟩
    simp only [Finset.sup_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · exact sup_factors_of_factors_left h
    · exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{v₁, u₁} C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
empty : ∀ (h : ∃ (i : I), Membership.mem (γ := Finset I) ∅ i ∧ (P i).Factors f), (Finset.sup ∅ P).Factors f
⊢ ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
have insert : ∀ (a : I) (s : Finset I),
  a ∉ s →
    ∀ (ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f) (h : ∃ i ∈ insert a s, (P i).Factors f),
      ((insert a s).sup P).Factors f
Tactic: induction s using Finset.induction_on with
  | empty => rintro ⟨_, ⟨⟨⟩, _⟩⟩
  | insert _ _ _ ih =>
    rintro ⟨j, ⟨m, h⟩⟩
    simp only [Finset.sup_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · exact sup_factors_of_factors_left h
    · exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{v₁, u₁} C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
h : ∃ i ∈ s, (P i).Factors f
⊢ (s.sup P).Factors f
have revert : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
Tactic: classical
  revert h
  induction s using Finset.induction_on with
  | empty => rintro ⟨_, ⟨⟨⟩, _⟩⟩
  | insert _ _ _ ih =>
    rintro ⟨j, ⟨m, h⟩⟩
    simp only [Finset.sup_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · exact sup_factors_of_factors_left h
    · exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)
Cleared hypotheses: h
-- 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 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
j : (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) : Type w)
⊢ Membership.mem (α := Subobject.{v₁, u₁} A) s
    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)) :
      Subobject.{v₁, u₁} A)
have rcases : ∀ (g : Subobject.{v₁, u₁} A) (m : g ∈ s),
  Membership.mem (α := Subobject.{v₁, u₁} A) s
    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) g) sorry) :
          Shrink.{w, max u₁ v₁} (Subobject A)) :
      Subobject.{v₁, u₁} A)
Tactic: rcases j with ⟨-, ⟨g, ⟨m, rfl⟩⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
⊢ sInf.{w, v₁, u₁} s ≤ f
have f₁ : Functor.obj underlying (sInf.{w, v₁, u₁} s) ⟶ Functor.obj underlying f
Tactic: fapply le_of_comm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
⊢ f ≤ sInf.{w, v₁, u₁} s
have f₁ : Functor.obj underlying f ⟶ Functor.obj underlying (sInf.{w, v₁, u₁} s)
Tactic: fapply le_of_comm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
f₁ : Functor.obj underlying f ⟶ Functor.obj underlying (sInf.{w, v₁, u₁} s)
⊢ f ≤ sInf.{w, v₁, u₁} s
have w : (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫ (sInf.{w, v₁, u₁} s).arrow =
  f.arrow
Tactic: fapply le_of_comm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (sInf.{w, v₁, u₁} s).arrow =
    f.arrow
have w : (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
    (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
  f.arrow
Tactic: dsimp [sInf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow
have w : limit.lift (wideCospan s) (leInfCone s f k) ≫
    Iso.inv (underlyingIso (widePullbackι s)) ≫ (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
  f.arrow
Tactic: rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
w :
  limit.lift (wideCospan s) (leInfCone s f k) ≫
      Iso.inv (underlyingIso (widePullbackι s)) ≫ (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow
have w₁ : CategoryStruct.comp (Y :=
    limit.{w, w, v₁, u₁} (J :=
      WidePullbackShape
        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
          Type w))
      (wideCospan s :
        Functor.{w, v₁, w, u₁}
          (WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          C))
    (limit.lift (wideCospan s) (leInfCone s f k) :
      Cone.pt.{w, v₁, w, u₁} (J :=
          WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          (F :=
          (wideCospan s :
            Functor.{w, v₁, w, u₁}
              (WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              C))
          (leInfCone s f k) ⟶
        limit.{w, w, v₁, u₁} (J :=
          WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          (wideCospan s :
            Functor.{w, v₁, w, u₁}
              (WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              C))
    (widePullbackι s : widePullback.{w, v₁, u₁} s ⟶ A) =
  f.arrow
Tactic: rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
w :
  limit.lift (wideCospan s) (leInfCone s f k) ≫
      Iso.inv (underlyingIso (widePullbackι s)) ≫ (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow
w₁ :
  CategoryStruct.comp (Y :=
      limit.{w, w, v₁, u₁} (J :=
        WidePullbackShape
          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
            Type w))
        (wideCospan s :
          Functor.{w, v₁, w, u₁}
            (WidePullbackShape
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w))
            C))
      (limit.lift (wideCospan s) (leInfCone s f k) :
        Cone.pt.{w, v₁, w, u₁} (J :=
            WidePullbackShape
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w))
            (F :=
            (wideCospan s :
              Functor.{w, v₁, w, u₁}
                (WidePullbackShape
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w))
                C))
            (leInfCone s f k) ⟶
          limit.{w, w, v₁, u₁} (J :=
            WidePullbackShape
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w))
            (wideCospan s :
              Functor.{w, v₁, w, u₁}
                (WidePullbackShape
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w))
                C))
      (widePullbackι s : widePullback.{w, v₁, u₁} s ⟶ A) =
    f.arrow
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow
have w₂ : CategoryStruct.comp (Y :=
    limit.{w, w, v₁, u₁} (J :=
      WidePullbackShape
        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
          Type w))
      (wideCospan s :
        Functor.{w, v₁, w, u₁}
          (WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          C))
    (limit.lift (wideCospan s) (leInfCone s f k)) (limit.π (wideCospan s) none) =
  f.arrow
Tactic: rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
⊢ f ≤ sSup.{w, v₁, u₁} s
have f₁ : Functor.obj underlying f ⟶ Functor.obj underlying (sSup.{w, v₁, u₁} s)
Tactic: fapply le_of_comm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
⊢ Functor.obj underlying f ⟶ Functor.obj underlying (sSup.{w, v₁, u₁} s)
have f₁ : Functor.obj underlying f =
  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
      (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
            Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
              ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
              x)
            ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) sorry) :
        Shrink.{w, max u₁ v₁} (Subobject A)))
Tactic: refine eqToHom ?_ ≫ Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩
      ≫ factorThruImage _ ≫ (underlyingIso _).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
⊢ sSup.{w, v₁, u₁} s ≤ f
have f₁ : Functor.obj underlying (sSup.{w, v₁, u₁} s) ⟶ Functor.obj underlying f
Tactic: fapply le_of_comm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
⊢ Functor.obj underlying (sSup.{w, v₁, u₁} s) ⟶ Functor.obj underlying f
have f₁ : (sigmaObj.{w, v₁, u₁}
    fun
      (j :
        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
          Type w)) ↦
    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
  Functor.obj underlying f
Tactic: refine (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
⊢ (sigmaObj.{w, v₁, u₁}
      fun
        (j :
          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
            Type w)) ↦
      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
          (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
    Functor.obj underlying f
have f₁ : (b :
    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
      Type w)) →
  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑b : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
    Functor.obj underlying f
Tactic: refine Sigma.desc ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)
m :
  Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
    ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) g
⊢ Functor.obj (C := Subobject.{v₁, u₁} A) underlying
      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              g m) :
          Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
    Functor.obj underlying f
have f₁ : Membership.mem (α := Subobject.{v₁, u₁} A) s
  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
      (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
            Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
              ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
              x)
            g m) :
        Shrink.{w, max u₁ v₁} (Subobject A)) :
    Subobject.{v₁, u₁} A)
Tactic: refine underlying.map (homOfLE (k _ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
⊢ Subsingleton (Subobject.{v₁, u₁} X)
have suffices : ∀ (S : Subobject.{v₁, u₁} X), S = mk (𝟙 X)
Tactic: suffices ∀ (S : Subobject X), S = .mk (𝟙 _) from ⟨by simp [this]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
S : Subobject.{v₁, u₁} X
⊢ S = mk (𝟙 X)
have obtain : ∀ (A : C) (i : A ⟶ X) (w : Mono i), mk i = mk (𝟙 X)
Tactic: obtain ⟨A, i, _, rfl⟩ := S.mk_surjective
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
⊢ mk i = mk (𝟙 X)
have fac : hX.to A ≫ i = 𝟙 X
Tactic: have fac : hX.to A ≫ i = 𝟙 X := hX.hom_ext _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
⊢ i ≫ hX.to A = 𝟙 A
have rw : (i ≫ hX.to A) ≫ i = 𝟙 A ≫ i
Tactic: rw [← cancel_mono i, assoc, fac, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
rw : (i ≫ hX.to A) ≫ i = 𝟙 A ≫ i
⊢ i ≫ hX.to A = 𝟙 A
have rw₁ : i ≫ hX.to A ≫ i = 𝟙 A ≫ i
Tactic: rw [← cancel_mono i, assoc, fac, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
rw : (i ≫ hX.to A) ≫ i = 𝟙 A ≫ i
rw₁ : i ≫ hX.to A ≫ i = 𝟙 A ≫ i
⊢ i ≫ hX.to A = 𝟙 A
have rw₂ : i ≫ 𝟙 X = 𝟙 A ≫ i
Tactic: rw [← cancel_mono i, assoc, fac, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
rw : (i ≫ hX.to A) ≫ i = 𝟙 A ≫ i
rw₁ : i ≫ hX.to A ≫ i = 𝟙 A ≫ i
rw₂ : i ≫ 𝟙 X = 𝟙 A ≫ i
⊢ i ≫ hX.to A = 𝟙 A
have rw₃ : i ≫ 𝟙 X = i
Tactic: rw [← cancel_mono i, assoc, fac, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
rw : (i ≫ hX.to A) ≫ i = 𝟙 A ≫ i
rw₁ : i ≫ hX.to A ≫ i = 𝟙 A ≫ i
rw₂ : i ≫ 𝟙 X = 𝟙 A ≫ i
rw₃ : i ≫ 𝟙 X = i
⊢ i ≫ hX.to A = 𝟙 A
have rw₄ : i = i
Tactic: rw [← cancel_mono i, assoc, fac, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (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
X : C
Y : Subobject.{v₁, u₁} X
W Z : Subobject.{v₁, u₁} (Functor.obj underlying Y)
⊢ Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (W.arrow ≫ Y.arrow)) ⋯ ≤
      Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (Z.arrow ≫ Y.arrow)) ⋯ ↔
    W ≤ Z
have mp : Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (W.arrow ≫ Y.arrow)) sorry ≤
    Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (Z.arrow ≫ Y.arrow)) sorry →
  W ≤ Z
Tactic: constructor