α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i in s, 1 - ∑ i in s, (f i * ∏ j in filter (fun x => x < i) s, (1 - f j)) * ∏ j in filter (fun j => i < j) s, 1 =
    1 - ∑ i in s, f i * ∏ j in filter (fun x => x < i) s, (1 - f j)
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i in s, (1 - f i) = 1 - ∑ i in s, f i * ∏ j in filter (fun x => x < i) s, (1 - f j)
rw [prod_sub_ordered]
no goals
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝² : CommSemiring β
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i in s, 1 - ∑ i in s, (f i * ∏ j in filter (fun x => x < i) s, (1 - f j)) * ∏ j in filter (fun j => i < j) s, 1 =
    1 - ∑ i in s, f i * ∏ j in filter (fun x => x < i) s, (1 - f j)
simp