-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem finset_sup_factors {I : Type*} {A B : C} {s : Finset I} {P : I → Subobject B} {f : A ⟶ B}
    (h : ∃ i ∈ s, (P i).Factors f) : (s.sup P).Factors f

Proof state:
case insert.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ 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

Tactic:
simp only [Finset.mem_insert] at m

Result:
case insert.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ 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

Proof state:
case empty
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ ∅, (P i).Factors f) → (∅.sup P).Factors f

Tactic:
rintro ⟨_, ⟨⟨⟩, _⟩⟩

Result:
no goals

Proof state:
case insert.intro.intro.inr
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ 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⟩⟩)

Result:
no goals

Proof state:
case insert.intro.intro.inl
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
h : (P j).Factors f
a✝ : j ∉ s✝
⊢ (P j ⊔ s✝.sup P).Factors f

Tactic:
exact sup_factors_of_factors_left h

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ s, (P i).Factors f
⊢ (s.sup P).Factors f

Tactic:
revert h

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ s, (P i).Factors f) → (s.sup P).Factors f

Proof state:
case insert.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
m : j ∈ insert a✝¹ s✝
h : (P j).Factors f
⊢ ((insert a✝¹ s✝).sup P).Factors f

Tactic:
simp only [Finset.sup_insert]

Result:
case insert.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ 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

Proof state:
case insert.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ 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

Tactic:
rcases m with (rfl | m)

Result:
case insert.intro.intro.inl
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
h : (P j).Factors f
a✝ : j ∉ s✝
⊢ (P j ⊔ s✝.sup P).Factors f

case insert.intro.intro.inr
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ 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

Proof state:
case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
⊢ (∃ i ∈ insert a✝¹ s✝, (P i).Factors f) → ((insert a✝¹ s✝).sup P).Factors f

Tactic:
rintro ⟨j, ⟨m, h⟩⟩

Result:
case insert.intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
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 ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
m : j ∈ insert a✝¹ s✝
h : (P j).Factors f
⊢ ((insert a✝¹ s✝).sup P).Factors f