no goals
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf s P) f ↔ ∀ (i : I), i ∈ s → Factors (P i) f
classical
induction' s using Finset.induction_on with _ _ _ ih
. simp [top_factors]
. simp [ih]
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
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf ∅ P) f ↔ ∀ (i : I), i ∈ ∅ → Factors (P i) f

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
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : Factors (Finset.inf s✝ P) f ↔ ∀ (i : I), i ∈ s✝ → Factors (P i) f
⊢ Factors (Finset.inf (insert a✝¹ s✝) P) f ↔ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) f
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf s P) f ↔ ∀ (i : I), i ∈ s → Factors (P i) f
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
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : Factors (Finset.inf s✝ P) f ↔ ∀ (i : I), i ∈ s✝ → Factors (P i) f
⊢ Factors (Finset.inf (insert a✝¹ s✝) P) f ↔ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) f
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
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf ∅ P) f ↔ ∀ (i : I), i ∈ ∅ → Factors (P i) f

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
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : Factors (Finset.inf s✝ P) f ↔ ∀ (i : I), i ∈ s✝ → Factors (P i) f
⊢ Factors (Finset.inf (insert a✝¹ s✝) P) f ↔ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) f
. simp [top_factors]
no goals
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
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : Factors (Finset.inf s✝ P) f ↔ ∀ (i : I), i ∈ s✝ → Factors (P i) f
⊢ Factors (Finset.inf (insert a✝¹ s✝) P) f ↔ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) f
. simp [ih]
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
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf ∅ P) f ↔ ∀ (i : I), i ∈ ∅ → Factors (P i) f
simp [top_factors]
no goals
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
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : Factors (Finset.inf s✝ P) f ↔ ∀ (i : I), i ∈ s✝ → Factors (P i) f
⊢ Factors (Finset.inf (insert a✝¹ s✝) P) f ↔ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) f
simp [ih]