C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ (∃ i, i ∈ s ∧ Factors (P i) f) → Factors (Finset.sup s P) f
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
h : ∃ i, i ∈ s ∧ Factors (P i) f
⊢ Factors (Finset.sup s P) f
revert h
case empty
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ (∃ i, i ∈ ∅ ∧ Factors (P i) f) → Factors (Finset.sup ∅ P) f

case insert
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
⊢ (∃ i, i ∈ insert a✝¹ s✝ ∧ Factors (P i) f) → Factors (Finset.sup (insert a✝¹ s✝) P) f
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ (∃ i, i ∈ s ∧ Factors (P i) f) → Factors (Finset.sup s P) f
induction' s using Finset.induction_on with _ _ _ ih
no goals
case empty
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ (∃ i, i ∈ ∅ ∧ Factors (P i) f) → Factors (Finset.sup ∅ P) f
rintro ⟨_, ⟨⟨⟩, _⟩⟩
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
m : j ∈ insert a✝¹ s✝
h : Factors (P j) f
⊢ Factors (Finset.sup (insert a✝¹ s✝) P) f
case insert
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
⊢ (∃ i, i ∈ insert a✝¹ s✝ ∧ Factors (P i) f) → Factors (Finset.sup (insert a✝¹ s✝) P) f
rintro ⟨j, ⟨m, h⟩⟩
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
m : j ∈ insert a✝¹ s✝
h : Factors (P j) f
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
m : j ∈ insert a✝¹ s✝
h : Factors (P j) f
⊢ Factors (Finset.sup (insert a✝¹ s✝) P) f
simp only [Finset.sup_insert]
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
m : j = a✝¹ ∨ j ∈ s✝
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
m : j ∈ insert a✝¹ s✝
h : Factors (P j) f
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
simp at m
case insert.intro.intro.inl
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
s✝ : Finset I
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
a✝ : ¬j ∈ s✝
⊢ Factors (P j ⊔ Finset.sup s✝ P) f

case insert.intro.intro.inr
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
m : j ∈ s✝
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
m : j = a✝¹ ∨ j ∈ s✝
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
rcases m with (rfl | m)
no goals
case insert.intro.intro.inl
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
s✝ : Finset I
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
a✝ : ¬j ∈ s✝
⊢ Factors (P j ⊔ Finset.sup s✝ P) f
exact sup_factors_of_factors_left h
no goals
case insert.intro.intro.inr
C : Type u₁
inst✝⁵ : Category C
X Y Z : C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
m : j ∈ s✝
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)