ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
⊢ (⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J) = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
⊢ Prepartition.iUnion (ofWithBot boxes le_of_mem pairwise_disjoint) = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
suffices (⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J) = ⋃ J ∈ boxes, (J : Set (ι → ℝ)) by
  simpa [ofWithBot, Prepartition.iUnion]
no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
⊢ (⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J) = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
simp only [← Box.biUnion_coe_eq_coe, @iUnion_comm _ _ (Box ι), @iUnion_comm _ _ (@Eq _ _ _),
  iUnion_iUnion_eq_right]
no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
this : (⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J) = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
⊢ Prepartition.iUnion (ofWithBot boxes le_of_mem pairwise_disjoint) = ⋃ (J : WithBot (Box ι)) (_ : J ∈ boxes), ↑J
simpa [ofWithBot, Prepartition.iUnion]