ι : Type u_1
M : Type ?u.58340
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) =
    Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂)
ι : Type u_1
M : Type ?u.58340
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ compl π₁ = compl π₂
dsimp only [compl]
case e_p
ι : Type u_1
M : Type ?u.58340
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ (fun π' => Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) = fun π' =>
    Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂
ι : Type u_1
M : Type ?u.58340
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) =
    Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂)
congr 1
no goals
case e_p
ι : Type u_1
M : Type ?u.58340
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ (fun π' => Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) = fun π' =>
    Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂
rw [h]