case refine'_1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(parallelepiped (Pi.basisFun ℝ ι)) = uIcc (fun i => 0) fun i => 1

case refine'_2
ι : Type u_1
inst✝ : Fintype ι
⊢ (fun i => 0) ≤ fun i => 1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(parallelepiped (Pi.basisFun ℝ ι)) = ↑(PositiveCompacts.piIcc01 ι)
refine' Eq.trans _ ((uIcc_of_le _).trans (Set.pi_univ_Icc _ _).symm)
no goals
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(parallelepiped (Pi.basisFun ℝ ι)) = uIcc (fun i => 0) fun i => 1
classical convert parallelepiped_single (ι := ι) 1
no goals
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(parallelepiped (Pi.basisFun ℝ ι)) = uIcc (fun i => 0) fun i => 1
convert parallelepiped_single (ι := ι) 1
no goals
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
⊢ (fun i => 0) ≤ fun i => 1
exact zero_le_one