case mk.mk
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
s₁ : Finset (Box ι)
h₁ : ∀ (J : Box ι), J ∈ s₁ → J ≤ I
h₁' : Set.Pairwise (↑s₁) (Disjoint on Box.toSet)
h₂ : ∀ (J : Box ι), J ∈ s₁ → J ≤ I
h₂' : Set.Pairwise (↑s₁) (Disjoint on Box.toSet)
⊢ { boxes := s₁, le_of_mem' := h₁, pairwiseDisjoint := h₁' } =
    { boxes := s₁, le_of_mem' := h₂, pairwiseDisjoint := h₂' }
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ Injective boxes
rintro ⟨s₁, h₁, h₁'⟩ ⟨s₂, h₂, h₂'⟩ (rfl : s₁ = s₂)
no goals
case mk.mk
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
s₁ : Finset (Box ι)
h₁ : ∀ (J : Box ι), J ∈ s₁ → J ≤ I
h₁' : Set.Pairwise (↑s₁) (Disjoint on Box.toSet)
h₂ : ∀ (J : Box ι), J ∈ s₁ → J ≤ I
h₂' : Set.Pairwise (↑s₁) (Disjoint on Box.toSet)
⊢ { boxes := s₁, le_of_mem' := h₁, pairwiseDisjoint := h₁' } =
    { boxes := s₁, le_of_mem' := h₂, pairwiseDisjoint := h₂' }
rfl