awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
empty : ∀ (i : I) (m : Membership.mem (γ := Finset I) ∅ i), (P i).Factors (Finset.inf ∅ P).arrow
insert :
  ∀ (a : I) (s : Finset I),
    a ∉ s →
      ∀ (ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow) (i : I) (m : i ∈ Insert.insert a s),
        (P i).Factors ((Insert.insert a s).inf P).arrow
⊢ ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow

Tactic:
induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m

Premises used: CategoryTheory.Subobject.inf_arrow_factors_right, Insert.insert, CategoryTheory.Subobject.factors_comp_arrow, Finset.mem_insert, Finset.inf_insert, CategoryTheory.Subobject.factors_of_factors_right, CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.Subobject.inf_arrow_factors_left, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
i : I
m : i ∈ s
revert : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
⊢ (P i).Factors (s.inf P).arrow

Tactic:
classical
  revert i m
  induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m

Premises used: CategoryTheory.Subobject.inf_arrow_factors_right, Insert.insert, CategoryTheory.Subobject.factors_comp_arrow, Finset.mem_insert, Finset.inf_insert, CategoryTheory.Subobject.factors_of_factors_right, CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.Subobject.inf_arrow_factors_left, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ : MonoOver.{v₁, u₁} A
f₂ : Subobject.{v₁, u₁} A
h :
  ∀ (a : MonoOver.{v₁, u₁} A),
    (Functor.obj inf (Quotient.mk'' f₁)).obj (Quotient.mk'' a) =
      (map f₁.arrow).obj ((pullback f₁.arrow).obj (Quotient.mk'' a))
⊢ (Functor.obj inf (Quotient.mk'' f₁)).obj f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

Tactic:
induction f₂ using Quotient.inductionOn'
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ a : MonoOver.{v₁, u₁} A
⊢ (Functor.obj inf (Quotient.mk'' f₁)).obj (Quotient.mk'' a) =
    (map f₁.arrow).obj ((pullback f₁.arrow).obj (Quotient.mk'' a))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
⊢ (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj f₂ =
    (map (Functor.obj representative f₁).arrow).obj ((pullback (Functor.obj representative f₁).arrow).obj f₂)

Tactic:
inf_eq_map_pullback' (representative.obj f₁) f₂

Premises used: CategoryTheory.Subobject.inf_eq_map_pullback', CategoryTheory.Subobject.representative, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
h : ∀ (x : Subobject.{v₁, u₁} A), f₁ ⊓ x = (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj x
⊢ min f₁ = (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ x : Subobject.{v₁, u₁} A
h :
  ThinSkeleton.mk (Functor.obj representative f₁) ⊓ x =
    (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj x
⊢ f₁ ⊓ x = (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj x

Tactic:
nth_rw 1 [← thinSkeleton_mk_representative_eq_self f₁]

Premises used: CategoryTheory.Subobject.thinSkeleton_mk_representative_eq_self
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ x : Subobject.{v₁, u₁} A
⊢ ThinSkeleton.mk (Functor.obj representative f₁) ⊓ x =
    (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj x

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
a : (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂
a₁ : f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)
⊢ (f₁ ⨯ f₂) = f₁ ⊓ f₂

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂

Tactic:
le_inf _ _ _ (Limits.prod.fst.le) (Limits.prod.snd.le)

Premises used: Quiver.Hom.le, CategoryTheory.Limits.prod.fst, CategoryTheory.Limits.prod.snd, CategoryTheory.Subobject.le_inf
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂

Tactic:
refine le_inf _ _ _ (Limits.prod.fst.le) (Limits.prod.snd.le)

Premises used: Quiver.Hom.le, CategoryTheory.Limits.prod.fst, CategoryTheory.Limits.prod.snd, CategoryTheory.Subobject.le_inf
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
a : f₁ ⊓ f₂ ⟶ f₁ ⨯ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)

Tactic:
apply leOfHom

Premises used: CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ⟶ f₁ ⨯ f₂

Tactic:
exact prod.lift (inf_le_left _ _).hom (inf_le_right _ _).hom

Premises used: CategoryTheory.Subobject.inf_le_left, LE.le.hom, CategoryTheory.Subobject.inf_le_right, CategoryTheory.Limits.prod.lift
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
m m' : Subobject.{v₁, u₁} B
⊢ m ⊓ m' = (Functor.obj inf m).obj m'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : X ⟶ Y
f₁ f₂ : Subobject.{v₁, u₁} Y
revert : ∀ (f₁ : Subobject.{v₁, u₁} Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
⊢ (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

Tactic:
revert f₁
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : X ⟶ Y
f₂ : Subobject.{v₁, u₁} Y
h :
  ∀ (a : MonoOver.{v₁, u₁} Y),
    (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂
⊢ ∀ (f₁ : Subobject.{v₁, u₁} Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

Tactic:
apply Quotient.ind'
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : X ⟶ Y
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
h :
  Functor.obj (C := Subobject.{v₁, u₁} (Limits.pullback f₁.arrow g)) (map (pullback.snd f₁.arrow g))
      (Functor.obj (pullback (pullback.snd f₁.arrow g ≫ g)) f₂) =
    (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂

Tactic:
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← pullback_comp, ←
    map_pullback pullback.condition (pullbackIsPullback f₁.arrow g), ← pullback_comp,
    pullback.condition]

Premises used: CategoryTheory.Subobject.map_pullback, CategoryTheory.Subobject.inf_eq_map_pullback', CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Subobject.inf_def, CategoryTheory.Subobject.pullback_comp, CategoryTheory.Limits.pullback.condition, CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : X ⟶ Y
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
⊢ Functor.obj (C := Subobject.{v₁, u₁} (Limits.pullback f₁.arrow g)) (map (pullback.snd f₁.arrow g))
      (Functor.obj (pullback (pullback.snd f₁.arrow g ≫ g)) f₂) =
    (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₁ f₂ : Subobject.{v₁, u₁} Y
revert : ∀ (f₁ : Subobject.{v₁, u₁} Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂
⊢ (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

Tactic:
revert f₁
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
h : ∀ (a : MonoOver.{v₁, u₁} Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map g).obj f₂
⊢ ∀ (f₁ : Subobject.{v₁, u₁} Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

Tactic:
apply Quotient.ind'
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
h :
  (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂

Tactic:
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← map_comp]

Premises used: CategoryTheory.Subobject.map_comp, CategoryTheory.Subobject.inf_eq_map_pullback', CategoryTheory.Subobject.inf_def
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
h :
  (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
h :
  (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj ((pullback g).obj ((map g).obj f₂)))
h₁ h₂ : (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) = (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂)
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))

Tactic:
rw [pullback_comp, pullback_map_self]

Premises used: CategoryTheory.Subobject.pullback_map_self, CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
A B : C
X Y : Subobject.{v₁, u₁} B
f : A ⟶ B
P : X.Factors f
⊢ (X ⊔ Y).Factors f

Tactic:
factors_of_le f le_sup_left P

Premises used: le_sup_left, CategoryTheory.Subobject.factors_of_le
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
A B : C
X Y : Subobject.{v₁, u₁} B
f : A ⟶ B
P : Y.Factors f
⊢ (X ⊔ Y).Factors f

Tactic:
factors_of_le f le_sup_right P

Premises used: le_sup_right, CategoryTheory.Subobject.factors_of_le
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
revert : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
⊢ (s.sup P).Factors f

Tactic:
revert h
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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.insert a s
h : (P j).Factors f
insert : (P a ⊔ s.sup P).Factors f
⊢ ((Insert.insert a s).sup P).Factors f

Tactic:
simp only [Finset.sup_insert]

Premises used: Finset.sup_insert
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
⊢ j = a ∨ j ∈ s

Tactic:
simp only [Finset.mem_insert] at m

Premises used: Finset.mem_insert
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
insert₁ : ∀ (m : j ∈ s), (P a ⊔ s.sup P).Factors f
⊢ (P a ⊔ s.sup P).Factors f

Tactic:
rcases m with (rfl | m)

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
s : Finset I
ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
j : I
h : (P j).Factors f
h_1 : j ∉ s
⊢ (P j ⊔ s.sup P).Factors f

Tactic:
sup_factors_of_factors_left h

Premises used: CategoryTheory.Subobject.sup_factors_of_factors_left
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
s : Finset I
ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
j : I
h : (P j).Factors f
h_1 : j ∉ s
⊢ (P j ⊔ s.sup P).Factors f

Tactic:
exact sup_factors_of_factors_left h

Premises used: CategoryTheory.Subobject.sup_factors_of_factors_left
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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 ∈ s
⊢ (P a ⊔ s.sup P).Factors f

Tactic:
sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)

Premises used: And.intro, Exists.intro, CategoryTheory.Subobject.sup_factors_of_factors_right
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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 ∈ s
⊢ (P a ⊔ s.sup P).Factors f

Tactic:
exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)

Premises used: And.intro, Exists.intro, CategoryTheory.Subobject.sup_factors_of_factors_right
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
insert :
  ∀ (a : I) (s : Finset I),
    a ∉ s →
      ∀ (ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f) (h : ∃ i ∈ Insert.insert a s, (P i).Factors f),
        ((Insert.insert a s).sup P).Factors f
⊢ ∀ (h : ∃ i ∈ s, (P i).Factors f), (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⟩⟩)

Premises used: Finset.sup_insert, Insert.insert, Finset.mem_insert, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
revert : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).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⟩⟩)

Premises used: Finset.sup_insert, Insert.insert, Finset.mem_insert, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
j : (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) : Type w)
⊢ Eq (α :=
    Functor.obj
        (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)
        (some j) ⟶
      Functor.obj.{w, v₁, w, u₁} (C :=
        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)
        (none :
          Option
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w)))
    (Functor.map (wideCospan s) (WidePullbackShape.Hom.term j) :
      Functor.obj
          (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)
          (some j) ⟶
        Functor.obj.{w, v₁, w, u₁} (C :=
          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)
          (none :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))
    (arrow
        ((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 (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))) ⟶
        A)

Tactic:
rfl

Premises used: CategoryTheory.Subobject.arrow, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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)
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) ⋯) :
            Shrink.{w, max u₁ v₁} (Subobject A)) :
        Subobject.{v₁, u₁} A)
⊢ 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)

Tactic:
rcases j with ⟨-, ⟨g, ⟨m, rfl⟩⟩⟩

Premises used: rfl