C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
⊢ ∀ (i : I), i ∈ s → Factors (P i) (arrow (Finset.inf s P))
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
i : I
m : i ∈ s
⊢ Factors (P i) (arrow (Finset.inf s P))
revert i m
case empty
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
⊢ ∀ (i : I), i ∈ ∅ → Factors (P i) (arrow (Finset.inf ∅ P))

case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
⊢ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) (arrow (Finset.inf (insert a✝¹ s✝) P))
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
⊢ ∀ (i : I), i ∈ s → Factors (P i) (arrow (Finset.inf s P))
induction' s using Finset.induction_on with _ _ _ ih
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
⊢ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) (arrow (Finset.inf (insert a✝¹ s✝) P))
case empty
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
⊢ ∀ (i : I), i ∈ ∅ → Factors (P i) (arrow (Finset.inf ∅ P))

case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
⊢ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) (arrow (Finset.inf (insert a✝¹ s✝) P))
. rintro _ ⟨⟩
no goals
case empty
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
⊢ ∀ (i : I), i ∈ ∅ → Factors (P i) (arrow (Finset.inf ∅ P))
rintro _ ⟨⟩
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ Factors (P i✝) (arrow (Finset.inf (insert a✝¹ s✝) P))
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
⊢ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) (arrow (Finset.inf (insert a✝¹ s✝) P))
intro _ m
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ Factors (P i✝) (arrow (Finset.inf (insert a✝¹ s✝) P))
rw [Finset.inf_insert]
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ = a✝¹ ∨ i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
simp only [Finset.mem_insert] at m
case insert.inl
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
a✝ : ¬i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P))

case insert.inr
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
case insert
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ = a✝¹ ∨ i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
rcases m with (rfl | m)
case insert.inl
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
a✝ : ¬i✝ ∈ s✝
⊢ Factors (P i✝)
    (factorThru (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P)) (_ : Factors (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P))) ≫
      arrow (P i✝))
case insert.inl
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
a✝ : ¬i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P))
rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
no goals
case insert.inl
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
a✝ : ¬i✝ ∈ s✝
⊢ Factors (P i✝)
    (factorThru (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P)) (_ : Factors (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P))) ≫
      arrow (P i✝))
exact factors_comp_arrow _
case insert.inr
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝)
    (factorThru (Finset.inf s✝ P) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
        (_ : Factors (Finset.inf s✝ P) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))) ≫
      arrow (Finset.inf s✝ P))
case insert.inr
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
case insert.inr.h
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (Finset.inf s✝ P))
case insert.inr
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝)
    (factorThru (Finset.inf s✝ P) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
        (_ : Factors (Finset.inf s✝ P) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))) ≫
      arrow (Finset.inf s✝ P))
apply factors_of_factors_right
no goals
case insert.inr.h
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (Finset.inf s✝ P))
exact ih _ m