ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ card (filter (fun J => x ∈ ↑Box.Icc J) π.boxes) ≤ Fintype.card (Set ι)
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ card (filter (fun J => x ∈ ↑Box.Icc J) π.boxes) ≤ 2 ^ Fintype.card ι
rw [← Fintype.card_set]
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ ∀ (a₁ : Box ι),
    a₁ ∈ filter (fun J => x ∈ ↑Box.Icc J) π.boxes →
      ∀ (a₂ : Box ι),
        a₂ ∈ filter (fun J => x ∈ ↑Box.Icc J) π.boxes →
          (fun J => {i | Box.lower J i = x i}) a₁ = (fun J => {i | Box.lower J i = x i}) a₂ → a₁ = a₂
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ card (filter (fun J => x ∈ ↑Box.Icc J) π.boxes) ≤ Fintype.card (Set ι)
refine' Finset.card_le_card_of_inj_on (fun J : Box ι => { i | J.lower i = x i })
  (fun _ _ => Finset.mem_univ _) _
no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
x : ι → ℝ
⊢ ∀ (a₁ : Box ι),
    a₁ ∈ filter (fun J => x ∈ ↑Box.Icc J) π.boxes →
      ∀ (a₂ : Box ι),
        a₂ ∈ filter (fun J => x ∈ ↑Box.Icc J) π.boxes →
          (fun J => {i | Box.lower J i = x i}) a₁ = (fun J => {i | Box.lower J i = x i}) a₂ → a₁ = a₂
simpa only [Finset.mem_filter] using π.injOn_setOf_mem_Icc_setOf_lower_eq x